Paradox in philosophy
C Problem set 3
In solving natural deduction problems, feel free to use either the sequent format (exempli�ed in the proof of LEM in section 9.3.3) or the box format (exempli�ed in �gure 9.3).
1. Natural deduction proofs Recall that we write`R for ‘entailment/validity under meaning as reasoning’—namely, specifying a particular system of rules of inference, we have Y `R ' when there is a derivation from Y of ' using those rules of inference.
Show the following, for the system of natural deduction rules from sec- tion 9.3.2:
(a) `R (('� )�')�' (Peirce’s Law) (b) `R ('� ( �⇢))� (('� )� ('�⇢)) (Frege’s Theorem) (c) Peirce’s Law `R LEM
three points each
2. Interderivability of rules We observed that the conception of meaning as reasoning has a built-in problem of ‘arbitrariness’—for anything you might want to accomplish, there are inde�nitely many super�cially di�erent ways to accomplish it.
These problems will give a �avour for this: collectively they show that ¬, together with any of ^, _, or �, can be used as the de�nitionally basic connectives in a natural deduction proof system.
(a) Interpreting _' as an abbreviation for¬(¬ ^¬'), use the intro- and elim-rules for ^ and ¬ to derive: i. The _-intro rule weakening ii. The _-elim rule dilemma
(b) Interpreting �' as an abbreviation for ¬ _', use the intro- and elim-rules for _ and ¬ to derive: i. The �-intro rule conditional proof
84 ������� ��� ���������
ii. The �-elim rule modus ponens (c) Now, using � and ¬ as the only connectives:
i. State an expression which can be used to de�ne ^'; ii. And, regarding ^' as an abbreviation for that expression, use the
intro and elim rules for � and ¬ to derive the ^-intro and -elim rules.
four points each
3. She�er stroke Taking this ‘arbitrariness’ to an extreme, there is a famous connective known as the She�er stroke—spelt ' | , it is de�ned as a ‘NAND’ operator, meaning (intuitively) not both ' and , or de�nable in terms of ^ and _ as ¬('^ ). The nifty thing about | is that it can be used as a sole primitive connective.
This has long been recognized in regard to a content-based characterization on which ~ | '� = N(~ �,~'�) := �(~ �\~'�). This N can be used to de�ne all other connectives—for example, with ~¬'� := N(~'�,~'�) and ~ ^'� := N(N(~ �,~'�)), N(~ �,~'�)). As we have seen, ^ and ¬ su�ce to de�ne everything else, so we are done.
But recently the analogous claim for the reasoning-based characterization has been demonstrated, by Richard Zach, who has published a cool natural deduction system for a language whose only connective is |, and which also contains an absurd sentence ?:
|-intro For all sentences ' and and sequents � for which there is a derivation from � + + ' of some � + + ' + . . .+?: – ::= � { � + | '
|-elim For all sentences ' and and sequents � = h. . . , ' | , ', i: – ::= � { � +?
?-elim For all sentences ' and sequents � = h. . . ,?i: – ::= � { � + '
Show that this system is just as powerful as the system using ^ and ¬:
(a) De�ne ¬ using the Sche�er stroke, and use the three |-rules to derive the three negation rules. four points
(b) Now do the same for conjunction. three points
4. Soundness Consider a language £� whose simple sentences include just those of form S i, for each natural number i; and whose complex sentences include just those of form ¬', ('^ ), and ('_ ) whenever ' and are sentences.
������� ��� 3 85
Now suppose that, for some nonempty set U of possibilities, £� is inter- preted using a context-independent semantic valuation function~·� mapping each sentence to a subset of U (so for each sentence ', we have ~'� ✓U). And suppose we know only the following about ~·�: for any ' and , ~¬'� = �~'�; ~ ^'� = ~ �\~'�; and ~ _'� = ~ �[~'�. Given these facts about the semantic valuation function, the natural deduc- tion rules in section 9.3.2 are sound, in the following sense:
For any set of sentences Y = { 1, . . . , n}and sentence ' (from the language £ �):
– If there is a derivation (using just those rules) from a sequent h 1, . . . , ni of a sequent h 1, . . . , n, . . . , 'i (namely: if Y `R ')
– Then: for any information state s ✓ U, and whatever the semantic valuation function ~·� may be (subject to the above constraints): – if : s ✓ ~ 1�\ · · ·\~ n� – then: s ✓ ~'� (namely: then Y `C ')
The way to establish soundness is one rule at a time: by showing that each of the individual rules is sound (namely, that whenever it is applied to a sequent � to yield a sequent �0, any info-state endorsing � also endorses �0)
• Show soundness for the negation rules ¬-I, ¬-E, and ¬¬-E.1 1 You may model your arguments on the soundness proofs in section 10.1.1. The second and third of these are easy; the
first is slightly more challenging. seven points (total)
5. Bonus question Now consider a language £+ with simple sentences just like those of £�, and whose formation rules for complex sentences include those of £� and also the rule that whenever ' is a sentence, so is �'. Now suppose that, for some nonempty set U of possibilities, and those info-states s ✓U, £� is interpreted using an info-state-dependent semantic valuation function~·�·· mapping each pair of a sentence and an info-state to a subset of U (so for each sentence ' and info-state s, we have ~'�s ✓U). And suppose we know only the following about ~·�··: for any s: for any simple sentence S i, there is some p for which ~S i�s = p; and for any ' and , ~¬'�s = �~'�s; ~ ^'�s = ~ �s \~'�s; ~ _'�s = ~ �s [~'�s; and ~�'�s = > just if s ✓ ~'�s, while otherwise ~�'�s = ?. But now the ¬-I rule is unsound.
(a) Show this. four bonus points
(b) Explain where the soundness proof for ¬-I breaks down. �ve bonus points