1

$((\neg \alpha \to \alpha) \to \alpha) $

Hi, I am trying to prove this.

Can someone gives me some hints to start the question... My friend told me I might need to use deduction theorem here, but I have no clue to approach it..

Axiom 1: A→(B→A).

Axiom 2: (A→(B→C))→((A→B)→(A→C)).

Axiom 3: (¬B→¬A)→((¬B→A)→B).

To clarify: A, B, C, α, and β are propositions (i.e. assigned True or False). → and ¬ have the standard logical meanings.

kengkeng
  • 129
  • 2
    What "Axiom 1,2,3" are supposed to be? It's difficult to help you in your question if you didn't provide enough information to do so. – Bruno Bentzen Nov 12 '14 at 04:57
  • 1
    Hints: Derive the law of identity (A$\rightarrow$A). Then make the antecedent of axiom 3 match an instance of the law of identity. – Doug Spoonwood Nov 12 '14 at 16:46
  • "Axiom 1,2,3"--what a confession. Someone needs to broaden his horizon a little. – George Chen Nov 13 '14 at 04:51
  • @GeorgeChen So I see you're a Russelian. Undoubtedly Russell and Whitehead derived several distinct axiom sets in their proofs in the disjunction-negation propositional calculus. How many bases did Russell and Whitehead derive which have no members in common with the 6-basis given by Russell and Whitehead? – Doug Spoonwood Nov 13 '14 at 06:38
  • @DougSpoonwood - Do you mean propositions commonly referred to by names, like Abs, Assoc, Syll and Fact? There are 16 of them among which Simp, Syll and Transp have multiple forms. Yes, they are all derived from primitive propositions, but they are nothing special per se, except that they are being frequently referred to by names. – George Chen Nov 13 '14 at 07:29
  • @DougSpoonwood- This (left side) is probably what you are talking abut: https://archive.org/stream/PrincipiaMathematicaVolumeI/WhiteheadRussell-PrincipiaMathematicaVolumeI#page/n11/mode/2up – George Chen Nov 13 '14 at 07:36
  • In PM, axioms or primitive propositions ( probably called basis in other books) are undefined, undemonstrated, i.e. not derived from other ideas or propositions. There is only one set of primitive ideas, primitive propositions and axioms. Whatever is derived from Pp is not called axiom any more. – George Chen Nov 13 '14 at 08:10
  • @GeorgeChen Inside that theory there exists only one set of primitive propositions and axioms. However, if you consider all axioms and theorems (or "theses" for both) as abbreviations for well-formed formulas, then outside the system several axiom sets get derived in the course of the proofs. For a better idea as to what I'm talking about, see this blog post: http://dougspoonwood.blogspot.com/ A. N. Prior lists several alternative bases to the Principia basis... in Polish notation, with "C" as an abbreviation for "AN" {CAppp, CqApq, CApqAqp, CApAqrAqApr, CCqrCApqApr} is Principia... – Doug Spoonwood Nov 13 '14 at 19:14
  • Some other bases are {CCApqrCpr, CCApqrCqr, CCprCCqrCApqr}, {CAppp, CpApq, CCpqCArpAqr}, {ApNApp, CpApq, CAqNpCArpAqr}, {CAppp, ApCpq, CApqCCqrApr}, {CApqAqApr, CpCqArp, CApqCCpq}, {CpApq, CApAqrCCqpArp}. With some of those bases in mind, it is likely that more bases can get extracted from the proofs of Principia Mathematica. – Doug Spoonwood Nov 13 '14 at 19:18
  • Also, if you look at string like *3.33, the "." symbol gets used in two different ways inside the string. The first "." indicates a conjunction. The second and third "." symbols indicate a bracketing of the formula such that a particular horseshoe symbol indicates the main connective. What rules could we state to disambiguate these "." symbols? – Doug Spoonwood Nov 13 '14 at 19:27
  • The use of dots is explained on page 9: https://archive.org/stream/PrincipiaMathematicaVolumeI/WhiteheadRussell-PrincipiaMathematicaVolumeI#page/n53/mode/2up – George Chen Nov 14 '14 at 07:54
  • It is very likely that W&R know these alternatives. As the authors state the preface, going back and forth and experimenting with premises make up the bulk of PM's labour of analysis. In the end, the authors can only affirm that the axioms they start with are sufficient, not necessary. – George Chen Nov 14 '14 at 08:29
  • Why they choose one set over another is extremely interesting. I think there is an underlying philosophy of mind. I remember, in several places, Russell said something like this: that is what people would naturally do if they had not known the controversies. – George Chen Nov 14 '14 at 08:44

4 Answers4

2

here's a proof without using the deduction theorem. I will use the Mendelson Axioms, which I think are the basic ones (or at least they are taught on a first course of logic). Hope it helps.

$1.- ¬a \implies ((¬a \implies ¬a) \implies ¬a )$ (Ax1)

$2.- (¬a \implies ((¬a \implies ¬a) \implies ¬a )) \implies ((¬a \implies (¬a \implies ¬a)) \implies (¬a \implies ¬a ))$ (Ax2)

$3.- (¬a \implies (¬a \implies ¬a)) \implies (¬a \implies ¬a ) $ (MP (1,2))

$4.- ¬a \implies (¬a \implies ¬a )$ (Ax1)

$5.- ¬a \implies ¬a $ (MP(3,4))

$6.- ( ¬a \implies ¬a) \implies (( ¬a \implies a) \implies a)$ (Ax3)

$7.- (¬a \implies a) \implies a $ (MP(5,6))

Di Alejandra
  • 182
  • From my reading of it St. Jaskowski's hinted at this axiom set in his paper "On the Rules of Supposition in Formal Logic" http://www.logik.ch/daten/jaskowski.pdf – Doug Spoonwood Nov 12 '14 at 16:41
1

I don't know what Axioms 1, 2, and 3 are. They are not standardized to that extent. But the following may help:

  1. Suppose $\neg\alpha \implies \alpha$.

  2. Suppose to the contrary that $\neg\alpha$.

  3. $\alpha$ (from 1 and 2).

  4. $\alpha \land \neg\alpha$ (from 3 and 2)

  5. $\neg\neg\alpha$ (from 2 and 4)

  6. $\alpha$ (from 5)

  7. $[\neg\alpha \implies \alpha]\implies \alpha$ (from 1 and 6)

Dan Christensen
  • 14,529
  • Hmmm... a 3-axiom basis with implication, negation, and conjunction. Well, using Prior's appendix it looks {CCCCCpqCNrNsrtCCtpCsp, CCKpqrCpCqr, CCpCqrCKpqr} it looks like that could work as such a basis. At least in principle. – Doug Spoonwood Nov 12 '14 at 05:08
1

Since I don't know your basis, I'll pick a three-axiom basis that I sometimes like which Elliot Mendelsohn uses (there is a suggestion that in some sense the basis can at least get said to have hinted at by Jaskowski in his original paper on Natural Deduction, "On the Rules Of Supposition in Formal Logic", if not earlier). I use Polish/Lukasiewicz notation, and condensed detachment.

axiom 1 C p Cqp.
axiom 2 C CpCqr C Cpq Cpr.
axiom 3 C CNpNq C CNpq p.
D2.1  4 C Cpq Cpp.
D4.1  5 Cpp.
D3.5  6 CCNppp.
Doug Spoonwood
  • 11,211
1

We can start with the "standard" proof of :

$\vdash \alpha \rightarrow \alpha$.

(1) $\alpha → ((\alpha \rightarrow \alpha) → \alpha)$ --- from Ax 1

(2) $(\alpha → ((\alpha \rightarrow \alpha) → \alpha)) → ((\alpha → (\alpha \rightarrow \alpha)) → (\alpha \rightarrow \alpha))$ --- from Ax 2

(3) $(\alpha → (\alpha \rightarrow \alpha)) → (\alpha \rightarrow \alpha)$ --- from (1) and (2) by MP

(4) $\alpha → (\alpha \rightarrow \alpha)$ --- from Ax 1

(5) $\alpha \rightarrow \alpha$ --- from (3) and (4) by MP

With it, Ax 1 and Ax 2, we can prove the Deduction Theorem.

Now for the proof of :

$\vdash (¬α→α)→α$

(1) $\vdash \lnot \alpha \rightarrow \lnot \alpha$ --- see above

(2) $\lnot \alpha \rightarrow \alpha$ --- assumed [a]

(3) $\vdash (\lnot \alpha \rightarrow \lnot \alpha) \rightarrow ((\lnot \alpha \rightarrow \alpha) \rightarrow \alpha)$ --- from Ax 3

(4) $\alpha$ --- from (1), (2) and (3) by MP twice

(5) $(\lnot \alpha \rightarrow \alpha) \rightarrow \alpha$ --- from (1) and (4) by Deduction Theorem

Mauro ALLEGRANZA
  • 94,169