Can Hilbert (style) prove my tautology?

Question

Can Hilbert (style) axioms prove the following tautology?

$$A\wedge(C\rightarrow B)\oplus(A\wedge B\leftrightarrow C)\rightarrow(C\rightarrow(A\rightarrow B))\qquad\text{algebraic style} $$$$ (((A\wedge(C\rightarrow B))\oplus((A\wedge B)\leftrightarrow C)))\rightarrow(C\rightarrow(A\rightarrow B))\qquad\text{formal style} $$

Here $\wedge$ means logical and, $\oplus$ means exclusive-or, and $\leftrightarrow$ means logical equivalence.

Due to Wikipedia/Hilbert style the axioms below describe classical propositional logic:

P1. $\phi \to \phi$

P2. $\phi \to \left( \psi \to \phi \right)$

P3. $\left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)$

P4. $\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)$

How to go? Is it necessary to add definitions of connectives?

Answer 1

You can see Elliott Mendelson, Introduction to mathematical logic (4ed - 1997) : PROPOSITION 1.14 (COMPLETENESS THEOREM).

The proof (due to Kalmar,1935) allows us to build a proof of a tautology $\mathcal B$ whatever.

Assume $\mathcal B$ is a tautology, and let $B_1, \ldots, B_k$ be the statement letetrs in $\mathcal B$. For any truth value assignment to $B_1, \ldots, B_k$ we have :

$B_1', \ldots, B_k' \vdash \mathcal B$

where let $B_i'$ be $B_i$ if $B_i$ takes the value $T$, and let $B_i'$ be $\lnot B_i$ if $B_i$ takes the value $F$.

Thus, due to the fact that your formula $\mathcal F$ has only three statement letters : $A,B,C$, it is enough to rewrite it in "primitive" notation, i.e. using only $\rightarrow$ and $\lnot$ (call it : $\mathcal F'$) and then apply the procedure described in the above Proposition.

Starting from example from the truth value assignment $v(A)=v(B)=v(C)=T$, we have :

$A,B,C \vdash \mathcal F'$.

Answer 2

To do this you would want to first define the other connectives. I will use Lukasiewicz/Polish notation. For your "∧" I write "K". For your "→" I write "C". For your "⊕", following A. N. Prior, I will write "J". For "$\lnot$", "N". For "↔" I will write E.

The axioms become

P2 CpCqp.

P3 CCpCqrCCpqCpr.

P4 CCNpNqCqp.

I will note that P1 is NOT an axiom given that a requirement for axioms is that they are independent, and I simply fail to understand this new standard where axioms don't have to be independent.

Now we'll need definitions for the other connectives, which in effect will end up behaving like axioms. The symbol "$\delta$" indicated a variable function of one argument. This means we can make substitutions for $\delta$.

PK: C$\delta$Kpq$\delta$NCpNq.

PE: C$\delta$Epq$\delta$NCCpqNCqp.

PJ: C$\delta$Jpq$\delta$CCpqNCqp.

Your formula is CJKaCcbEKabcCcCab.

Using definition PK we can tell that CJKaCcbEKabcCcCab is equivalent to

CJNCaNCcbENCaNbcCcCab.

Using definition PE we can tell that CJNCaNCcbENCaNbcCcCab is equivalent to

CJNCaNCcbNCCNCaNbcNCcNCaNbCcCab.

Using definiton PJ we can tell that CJNCaNCcbNCCNCaNbcNCcNCaNbCcCab is equivalent to

CCCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCaNbNCaNCcbCcCab.

To try to prove it using Prover9, or OTTER you'll only need to parenthesize all of the axioms and use a unary predicate (which you may think of as meaning "provable" or "is formally provable"), and rewrite the variables as "x", "y" and "z" respectively for "a", "c", and "b" or "p", "q" and "r"... something like this:

P2: P(C(x,C(y,x))).

P3: P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).

P4: P(C(C(N(x),N(y)),C(y,x))).

Parenthesize P(CCCNCxNCzyNCCNCxNyzNCzNCxNyNCNCCNCxNyzNCzNCxNyNCxNCzyCzCxy), and add this as the goal. This formula is:

 P(C(C(C(N(C(x,N(C(z,y)))),N(C(C(N(C(x,N(y))),z),N(C(z,N(C(x,N(y)))))))),N(C(N(C(C(N(C(x,N(y))),z),N(C(z,N(C(x,N(y))))))),N(C(x,N(C(z,y))))))),C(z,C(x,y)))).

You'll also want an assumption which enables Prover9 to prove things like it were using condensed detachment:

-P(C(x,y)) | -P(x) | P(y). (it is not the case that either it is provable that x implies y, or it is not the case that x is provable, or y is provable). Then you might find a proof equivalent to a proof using condensed detachment. You'll want to prove that since you have

PK: C$\delta$Kpq$\delta$NCpNq.

PE: C$\delta$Epq$\delta$NCCpqNCqp.

PJ: C$\delta$Jpq$\delta$CCpqNCqp.

you can prove

PK reversed: C $\delta$NCpNq $\delta$Kpq.

PE reversed: C $\delta$NCCpqNCqp $\delta$Epq.

PJ reversed: C $\delta$CCpqNCqp $\delta$Jpq.

And it does come as possible to prove each of those, since it has gotten proven that from

C $\delta$ P $\delta$ R

we can derive

C $\delta$ R $\delta$ P

where "R" and "P" are constants, and we only have substitution and detachment as the rules of inference.

Another approach could involve proving CCNpqCCNpNqp (or CCNpNqCCNpqp). Then one could set up a natural-deduction like demonstration of the C-N fomrula you've referred to, and then use the proof of the deduction meta-theorem to produce a formal proof.

Answer 3

I use condensed detachment notated by "D" in the proof analysis. Dx.y indicates that condensed detachment gets applied to formula x with form Cx y, and y has form x' such that x and x' have a most general unifier.

So we want to prove CCCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCaNbNCaNCcbCcCab. I'll note that as I worked through this proof I had to several times find the antecedent of a formula, or where particular formulas would "match". The simplicity of the algorithm for formulas in Lukasiewicz notation helped a lot! Here's a proof:

axiom      1 CxCyx. 
axiom      2 CCxCyzCCxyCxz. 
axiom      3 CCNxNyCyx. 
D1.1       4 CxCyCzy.
D2.2       5 CCCxCyzCxyCCxCyzCxz.
D1.5       6 CxCCCyCzuCyzCCyCzuCyu.
D2.1       7 CCxyCxx.
D7.1       8 Cxx.
D2.3       9 CCCNxNyyCCNxNyx.
D1.3      10 CxCCNyNzCzy.
D1.4      11 CxCyCzCuz.
D2.8      12 CCCxyxCCxyy.
D2.10     13 CCxCNyNzCxCzy.
D13.1     14 CNxCxy.
D13.14    15 CNNxCyx.
D2.14     16 CCNxxCNxy.
D1.14     17 CxCNyCyz.
D12.17    18 CCCNxCxyzz. 
D5.11     19 CCxCCyCzyuCxu.
D5.4      20 CCxCCyxzCxz.
D20.15    21 CNNxx.
D1.2      22 CxCCyCzuCCyzCyu.
D2.22     23 CCxCyCzuCxCCyzCyu.
D23.1     24 CCxyCCzxCzy.
D3.21     25 CxNNx.
D24.25    26 CCxyCxNNy.
D18.26    27 CNxNNCxy.
D13.26    28 CCNxyCNyx.
D3.27     29 CNCxyx.
D28.15    30 CNCxyNy.

break

D19.24    31 CCCxyzCyz.
D31.9     32 CxCCNyNxy.
D2.32     33 CCxCNyNxCxy.
D33.16    34 CCNxxx.
D1.23     35 CxCCyCzCuvCyCCzuCzv.
D2.35     36 CCxCyCzCuvCxCyCCzuCzv.
D1.36     37 CxCCyCzCuCvwCyCzCCuvCuw.
D2.37     38 CCxCyCzCuCvwCxCyCzCCuvCuw.
D1.38     39 CxCCyCzCuCvCwdCyCzCuCCvwCvd.
D2.39     40 CCxCyCzCuCvCwdCxCyCzCuCCvwCvd.
D1.21     41 CxCNNyy.
D1.41     42 CxCyCNNzz.
D1.42     43 CxCyCzCNNuu.
D1.43     44 CxCyCzCuCNNvv.
D1.44     45 CxCyCzCuCvCNNww. 
D40.45    46 CxCyCzCuCCvNNwCvw. 
D38.46    47 CxCyCzCCuCvNNwCuCvw. 
D1.30     48 CxCNCyzNz.
D1.48     49 CxCyCNCzuNu.
D1.49     50 CxCyCzCNCuvNv.
D1.50     51 CxCyCzCuCNCvwNw. 
D36.47    52 CxCyCCzCuCvNNwCzCuCvw. 
D23.52    53 CxCCyCzCuCvNNwCyCzCuCvw. 
D2.53     54 CCxCyCzCuCvNNwCxCyCzCuCvw. 
D54.51    55 CxCyCzCuCNCvNww. 
D24.1     56 CCxyCxCzy. 
D56.1     57 CxCyCzx. 
D1.57     58 CxCyCzCuy. 
D1.56     59 CxCCyzCyCuz.
D2.59     60 CCxCyzCxCyCuz.

break

D60.58    61 CxCyCzCuCvy. 
D40.55    62 CxCyCzCuCCNCvNCwdwCNCvNCwdd. 
D38.62    63 CxCyCzCCuCNCvNCwdwCuCNCvNCwdd. 
D36.63    64 CxCyCCzCuCNCvNCwdwCzCuCNCvNCwdd. 
D23.64    65 CxCCyCzCuCNCvNCwdwCyCzCuCNCvNCwdd. 
D2.65     66 CCxCyCzCuCNCvNCwdwCxCyCzCuCNCvNCwdd. 
D66.61    67 CxCyCzCuCNCvNCyww. 
D1.17     68 CxCyCNzCzu.
D1.68     69 CxCyCzCNuCuv.
D1.69     70 CxCyCzCuCNvCvw.
D1.70     71 CxCyCzCuCvCNwCwd. 
D40.71    72 CxCyCzCuCCvNwCvCwd. 
D38.72    73 CxCyCzCCuCvNwCuCvCwd. 
D36.73    74 CxCyCCzCuCvNwCzCuCvCwd. 
D23.74    75 CxCCyCzCuCvNwCyCzCuCvCwd. 
D1.11     76 CxCyCzCuCvu. 
D2.75     77 CCxCyCzCuCvNwCxCyCzCuCvCwd.
D77.76    78 CxCyCzCNuCvCuw. 
D40.78    79 CxCyCzCNuCCvuCvw. 
D38.79    80 CxCyCzCCNuCvuCNuCvw. 
D36.80    81 CxCyCCzCNuCvuCzCNuCvw. 
D34.81    82 CxCCyCzCNuCvuCyCzCNuCvw. 
D2.82     83 CCxCyCzCNuCvuCxCyCzCNuCvw. 
D83.67    84 CxCyCzCNuCNCvNCyuw. 
D56.57    85 CxCyCzCux. 
D38.85    86 CCxyCzCuCCvxCvy. 
D36.86    87 CCxyCzCCuCvxCuCvy. 
D23.87    88 CCxyCCzCuCvxCzCuCvy. 
D2.88     89 CCCxyCzCuCvxCCxyCzCuCvy.
D89.84    90 CCCNCxNCyzuvCyCwCNzv. 

break

D1.29     91 CxCNCyzy.
D1.91     92 CxCyCNCzuz.
D1.92     93 CxCyCzCNCuvu.
D1.93     94 CxCyCzCuCNCvwv. 
D38.94    95 CxCyCzCCuNCvwCuv. 
D36.95    96 CxCyCCzCuNCvwCzCuv. 
D23.96    97 CxCCyCzCuNCvwCyCzCuv. 
D2.97     98 CCxCyCzCuNCvwCxCyCzCuv.
D98.90    99 CCCNCxNCyzuNCvwCyCdCNzv. 
D38.51   100 CxCyCzCCuNCvwCuNw. 
D36.100  101 CxCyCCzCuNCvwCzCuNw. 
D34.101  102 CxCCyCzCuNCvwCyCzCuNw. 
D2.102   103 CCxCyCzCuNCvwCxCyCzCuNw.
D103.99  104 CCCNCxNCyzuNCNCvwdCyCeCNzNw. 
D38.44   105 CxCyCzCCuNNvCuv. 
D36.105  106 CxCyCCzCuNNvCzCuv. 
D23.106  107 CxCCyCzCuNNvCyCzCuv. 
D2.107   108 CCxCyCzCuNNvCxCyCzCuv.
D108.104 109 CCCNCxNCyzuNCNCvNwdCyCeCNzw. 
D38.109  110 CCCNCxNCyzuNCNCvNCwdeCyCfCCNzwCNzd. 
D36.110  111 CCCNCxNCyzuNCNCvNCwdeCyCCfCNzwCfCNzd. 
D23.111  112 CCCNCxNCyzuNCNCvNCwdeCCyCfCNzwCyCfCNzd.   
D2.112   113 CCCCNCxNCyzuNCNCvNCwdeCyCfCNzwCCCNCxNCyzuNCNCvNCwdeCyCfCNzd.
D113.11  114 CCCNCxNCyzuNCNCvNCwdeCyCwCNzd.
D23.114  115 CCCNCxNCyzuNCNCvNCwdeCCywCyCNzd. 
D2.115   116 CCCCNCxNCyzuNCNCvNCwdeCywCCCNCxNCyzuNCNCvNCwdeCyCNzd.
D1.8     117 CxCyy
D116.117 118 CCCNCxNCyzuNCNCvNCywdCyCNzw. 
D1.56    119 CxCCyzCyCuz.            
D2.119   120 CCxCyzCxCyCuz.

break

D120.118 121 CCCNCxNCyzuNCNCvNCywdCyCeCNzw.  
D23.101  122 CxCCyCzCuNCvwCyCzCuNw.  
D2.122   123 CCxCyCzCuNCvwCxCyCzCuNw. 
D123.121 124 CCCNCxNCyzuNCNCvNCyNCwdeCyCfCNzNd.
D108.124 125 CCCNCxNCyzuNCNCvNCyNCwNdeCyCfCNzd. 
D1.34    126 CxCCNyyy.
D1.126   127 CxCyCCNzzz.
D1.127   128 CxCyCzCCNuuu. 
D36.128  129 CxCyCCzCNuuCzu. 
D23.129  130 CxCCyCzCNuuCyCzu. 
D2.130   131 CCxCyCzCNuuCxCyCzu.
D131.125 132 CCCNCxNCyzuNCNCvNCyNCwNzdCyCez.

You might want to observe that 132 has eight variables. $\alpha$/$\beta$ indicates that formula $\alpha$ gets substituted with $\beta$.

132 x/a  133 CCCNCaNCyzuNCNCvNCyNCwNzdCyCez.
133 y/c  134 CCCNCaNCczuNCNCvNCcNCwNzdCcCez.
134 z/b  135 CCCNCaNCcbuNCNCvNCcNCwNbdCcCez.
135 u/NCCNCaNbcNCcNCaNb   136 CCCNCaNCcbNCCNCaNbcNCcNCaNbNCNCvNCcNCwNbdCcCeb.
136 v/CNCaNbc 137 CCCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCwNbdCcCeb.
137 w/a  138 CCCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCaNbdCcCeb.
138 d/NCaNCcb 139 CCCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCaNbNCaNCcbCcCeb.

So, CCCNCxNCyzuNCNCvNCyNCwNzdCyCez is a more general formula than 139. How did I prove something like CCCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCaNbNCaNCcbCcCab? First I set up a "natural deduction" style proof where all of the variables behave like constants. Then I assumed the antecedents "CCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCaNbNCaNCcb", "c", and "b". I thought that if I assumed the negation of the conclusion "Nb" I could then derive a contradiction. Then I would use the formula CCNxNyCCNxyx to get to "b". But how to do that? I've found that sometimes when you have a formula like CCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCaNbNCaNCcb, it can help to try and prove that its antecedent holds true... in this case "CNCaNCcbNCCNCaNbcNCcNCaNb". Then we can detach its consequent "CNCaNCcbNCCNCaNbcNCcNCaNb". So, if we assume NCaNCcb, can we get to NCCNCaNbcNCcNCaNb? Well, if we assume any negation of a conditional NCxy, we can infer that "x" holds and "Ny" holds. Now I did find another path than I originally got on, but trying to prove the antecedent of an assumed conditional did help, and inferring from a formula of the form NCxy to "x" and "Ny" did help here. Here's what I did for the set-up:

I used some lemmas:

L1. CNNxx.
L2. CNxCxy.
L3. CNCxyNy.
L4. CNCxyx.
L5. CCNxxx.

and set up the proof with this deduction:

hypothesis 1 | CCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCaNbNCaNCcb. (ante)
hypothesis 2 || c.
hypothesis 3 ||| a.
hypothesis 4 |||| Nb.
hypothesis 5 ||||| NCaNCcb.
D5.L3      6 ||||| NNCcb.
D(L1).6    7 ||||| Ccb.
D7.2       8 ||||| b.
D(L2).4    9 ||||| Cbx.
D9.8      10 ||||| x.
Ci 5-10   11 |||| CNCaNCcbx.
D1.11     12 |||| NCNCCNCaNbcNCcNCaNbNCaNCcb.
D(L4).12  13 |||| NCCNCaNbcNCcNCaNb
D(L3).13  14 |||| NNCcNCaNb.
D(L1).14  15 |||| CcNCaNb.
D15.2     16 |||| NCaNb.
D(L3).16  17 |||| NNb.
D(L1).17  18 |||| b.
Ci 4-18   19 ||| CNbb.
D(L5).19  20 ||| b.
Ci 3-20   21 || Cab.
Ci 2-21   22 | CcCab.
Ci 1-22   23 CCCNCaNCcbNCCNCaNbcNCcNCaNbNCNCCNCaNbcNCcNCaNbNCaNCcbCcCab.

Then I used the conversion procedure outlined by standard proofs of the Deduction Meta-Theorem along with condensed detachment.