Hilbert System - Automate Proof

https://stackoverflow.com/questions/1581256

21-09-2019
|

문제

I'm trying to prove the statement ~(a->~b) => a in a Hilbert style system. Unfortunately it seems like it is impossible to come up with a general algorithm to find a proof, but I'm looking for a brute force type strategy. Any ideas on how to attack this are welcome.

해결책

If You like "programming" in combinatory logic, then

You can automatically "translate" some logic problems into another field: proving equality of combinatory logic terms.
With a good functional programming practice, You can solve that,
and afterwards, You can translate the answer back to a Hilbert style proof of Your original logic problem.

The possibility of this translation in ensured by Curry-Howard correspondence.

Unfortunately, the situation is so simple only for a subset of (propositional) logic: restricted using conditionals. Negation is a complication, I know nothing about that. Thus I cannot answer this concrete question:

¬ (α ⊃ ¬β) ⊢ α

But in cases where negation is not part of the question, the mentioned automatic translation (and back-translation) can be a help, provided that You have already practice in functional programming or combinatory logic.

Of course, there are other helps, too, where we can remain inside the realm of logic:

proving the problem in some more intuitive deductive system (e.g. natural deduction)
and afterwards using metatheorems that provide a "compiler" possibility: translating the "high-level" proof of natural deduction to the "machine-code" of Hilbert-style deduction system. I mean, for example, the metalogical theorem called "deduction theorem".

As for theorem provers, as far as I know, the capabilities of some of them are extended so that they can harness interactive human assistance. E.g. Coq is such.

Appendix

Let us see an example. How to prove α ⊃ α?

Hilbert system

Verum ex quolibet_α,β is assumed as an axiom scheme, stating that sentence α ⊃ β ⊃ α is expected to be deducible, instantiated for any subsentences α,β
Chain rule_α,β,γ is assumed as an axiom scheme, stating that sentence (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α ⊃ γ is expected to be deducible, instantiated for any subsentences α,β
Modus ponens is assumed as a rule of inference: provided that α ⊃ β is deducible, and also α is deducible, then we expect to be justified to infer that also α ⊃ β is deducible.

Let us prove theorem: α ⊃ α is deducible for any α proposition.

Let us introduce the following notations and abbreviations, developing a "proof calculus":

Proof calculus

VEQ_α,β: ⊢ α ⊃ β ⊃ α
CR_α,β,γ: ⊢ (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ
MP: If ⊢ α ⊃ β and ⊢ α, then also ⊢ β

A tree diagram notation:

Axiom scheme — Verum ex quolibet:

━━━━━━━━━━━━━━━━━ [VEQ_α,β]
⊢ α ⊃ β ⊃ α

Axiom scheme — chain rule:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [CR_α,β,γ]
⊢ (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ

Rule of inference — modus ponens:

     ⊢ α ⊃ β           ⊢ α
    ━━━━━━━━━━━━━━━━━━━ [MP]
                     ⊢ β

Proof tree

Let us see a tree diagram representation of the proof:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [CR_{α, α⊃α, α}]    ━━━━━━━━━━━━━━━ [VEQ_{α, α⊃α}]
⊢ [α⊃(α⊃α)⊃α]⊃(α⊃α⊃α)⊃α⊃α                         ⊢ α ⊃ (α ⊃ α) ⊃ α
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [MP]      ━━━━━━━━━━━ [VEQ_α,α]
                                          ⊢ (α ⊃ α ⊃ α) ⊃ α ⊃ α                                              ⊢ α ⊃ α ⊃ α
                                          ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [MP]
                                                                                     ⊢ α ⊃ α

Proof formulae

Let us see an even conciser (algebraic? calculus?) representation of the proof:

(CR_{α,α⊃α,α} VEQ_{α,α ⊃ α}) VEQ_α,α: ⊢ α⊃ α

so, we can represent the proof tree by a single formula:

the forking of the tree (modus ponens) is rendered by simple concatenation (parentheses),
and the leaves of the tree are rendered by the abbreviations of the corresponding axiom names.

It is worth of keep record about the concrete instantiation, that' is typeset here with subindexical parameters.

As it will be seen from the series of examples below, we can develop a proof calculus, where axioms are notated as sort of base combinators, and modus ponens is notated as a mere application of its "premise" subproofs:

Example 1

VEQ_α,β: ⊢ α ⊃ β ⊃ α

meant as

Verum ex quolibet axiom scheme instantiated with α,β provides a proof for the statement, that α ⊃ β ⊃ α is deducible.

Example 2

VEQ_α,α: ⊢ α ⊃ α ⊃ α

Verum ex quolibet axiom scheme instantiated with α,α provides a proof for the statement, that α ⊃ α ⊃ α is deducible.

Example 3

VEQ_{α, α⊃α}: ⊢ α ⊃ (α ⊃ α) ⊃ α

meant as

Verum ex quolibet axiom scheme instantiated with α, α⊃α provides a proof for the statement, that α ⊃ (α ⊃ α) ⊃ α is deducible.

Example 4

CR_α,β,γ: ⊢ (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ

meant as

Chain rule axiom scheme instantiated with α,β,γ provides a proof for the statement, that (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α⊃ γ is deducible.

Example 5

CR_{α,α⊃α,α}: ⊢ [α ⊃ (α⊃α) ⊃ α] ⊃ (α ⊃ α⊃α) ⊃ α⊃ α

meant as

Chain rule axiom scheme instantiated with α,α⊃α,α provides a proof for the statement, that [α ⊃ (α⊃α) ⊃ α] ⊃ (α ⊃ α⊃α) ⊃ α⊃ α is deducible.

Example 6

CR_{α,α⊃α,α} VEQ_{α,α ⊃ α}: ⊢ (α ⊃ α⊃α) ⊃ α⊃ α

meant as

If we combine CR_{α,α⊃α,α} and VEQ_{α,α ⊃ α} together via modus ponens, then we get a proof that proves the following statement: (α ⊃ α⊃α) ⊃ α⊃ α is deducible.

Example 7

(CR_{α,α⊃α,α} VEQ_{α,α ⊃ α}) VEQ_α,α: ⊢ α⊃ α

If we combine the compund proof (CR_{α,α⊃α,α}) together with VEQ_{α,α ⊃ α} (via modus ponens), then we get an even more compund proof. This proves the following statement: α⊃ α is deducible.

Combinatory logic

Although all this above has indeed provided a proof for the expected theorem, but it seems very unintuitive. It cannot be seen how people can "find out" the proof.

Let us see another field, where similar problems are investigated.

Untyped combinatory logic

Combinatory logic can be regarded also as an extremely minimalistic functional programming language. Despite of its minimalism, it entirely Turing complete, but evenmore, one can write quite intuitive and complex programs even in this seemingly obfuscated language, in a modular and reusable way, with some practice gained from "normal" functional programming and some algebraic insights, .

Adding typing rules

Combinatory logic also has typed variants. Syntax is augmented with types, and evenmore, in addition to reduction rules, also typing rules are added.

For base combinators:

K_α,β is selected as a basic combinator, inhabiting type α → β → α
S_α,β,γ is selected as a basic combinator, inhabiting type (α → β → γ) → (α → β) → α → γ.

Typing rule of application:

If X inhabits type α → β and Y inhabits type α, then X Y inhabits type β.

Notations and abbreviations

K_α,β: α → β → α
S_α,β,γ: (α → β → γ) → (α → β)* → α → γ.
If X: α → β and Y: α, then X Y: β.

Curry-Howard correspondence

It can be seen that the "patterns" are isomorphic in the proof calculus and in this typed combinatory logic.

The Verum ex quolibet axiom of the proof calculus corresponds to the K base combinator of combinatory logic
The Chain rule axiom of the proof calculus corresponds to the S base combinator of combinatory logic
The Modus ponens rule of inference in the proof calculus corresponds to the operation "application" in combinatory logic.
The "conditional" connective ⊃ of logic corresponds to type constructor → of type theory (and typed combinatory logic)

Functional programming

But what is the gain? Why should we translate problems to combinatory logic? I, personally, find it sometimes useful, because functional programming is a thing which has a large literature and is applied in practical problems. People can get used to it, when forced to use it in erveryday programming tasks ans pracice. And some tricks and hints of functional programming practice can be exploited very well in combinatory logic reductions. And if a "transferred" practice develops in combinatory logic, then it can be harnessed also in finding proofs in Hilbert system.

External links

Links how types in functional programming (lambda calculus, combinatory logic) can be translated into logical proofs and theorems:

Wadler, Philip (1989). Theorems for free!.

Links (or books) how to learn methods and practice to program directly in combinatory logic:

Madore, David (2003). The Unlambda Programming Language. Unlambda: Your Functional Programming Language Nightmares Come True.
Curry, Haskell B. & Feys, Robert & Craig, William (1958). Combinatory Logic. Vol. I. Amsterdam: North-Holland Publishing Company.
Tromp, John (1999). Binary Lambda Calculus and Combinatory Logic. Downloadable in PDF and Postscript from the author's John's Lambda Calculus and Combinatory Logic Playground.

다른 팁

The Hilbert system is not normally used in automated theorem proving. It is much easier to write a computer program to do proofs using natural deduction. From the material of a CS course:

Some FAQ’s about the Hilbert system: Q: How does one know which axiom schemata to use, and which substitutions to make? Since there are infinitely many possibilities, it is not possible to try them all, even in princple. A: There is no algorithm; at least no simple one. Rather, one has to be clever. In pure mathematics, this is not viewed as a problem, since one is most concerned about the existence of a proof. However, in computer science applications, one is interested in automating the deduction process, so this is a fatal flaw. The Hilbert system is not normally used in automated theorem proving. Q: So, why do people care about the Hilbert system? A: With modus ponens as its single deductive rule, it provides a palatable model of how humans devise mathematical proofs. As we shall see, methods which are more amenable to computer implementation produce proofs which are less “human like.”

Finding proofs in Hilbert calculus is very hard.

You could try to translate proofs in sequent calculus or natural deduction to Hilbert calculus.

You can approach the problem also by setting ¬ α = α → ⊥. We can then adopt the Hilbert style system as shown in the appendix of one of the answers, and make it classical by adding the following two axioms respectively constants:

Ex Falso Quodlibet: E_α : ⊥ → α
Consequentia Mirabilis: M_α : (¬ α → α) → α

A sequent proof of ¬ (α → ¬ β) → α then reads as follows:

α ⊢ α (Identity)
⊥ ⊢ β → ⊥ (Ex Falso Quodlibet)
α → ⊥, α ⊢ β → ⊥ (Impl Intro Left 1 & 2)
α → ⊥ ⊢ α → (β → ⊥) (Impl Intro Right 3)
⊥ ⊢ α (Ex Falso Quodlibet)
(α → (β → ⊥)) → ⊥, α → ⊥ ⊢ α (Impl Intro Left 4 & 5)
(α → (β → ⊥)) → ⊥ ⊢ α (Consequentia Mirabilis 6)
⊢ ((α → (β → ⊥)) → ⊥) → α (Impl Intro Right 7)

From this sequent proof, one can extract a lambda expression. A possible lambda expressions for the above sequent proof reads as follows:

λy.(M λz.(E (y λx.(E (z x)))))

This lambda expression can be converted into a SKI term. A possible SKI term for the above lambda expression reads as follows:

S (K M)) (L2 (L1 (K (L2 (L1 (K I))))))
where L1 = (S ((S (K S)) ((S (K K)) I)))
and L2 = (S (K (S (K E))))

This gives the following Hilbert style proofs:

Lemma 1: A weakened form of the chain rule:
1: ((A → B) → ((C → A) → (C → B))) → (((A → B) → (C → A)) → ((A → B) → (C → B))) [Chain]
2: ((A → B) → ((C → (A → B)) → ((C → A) → (C → B)))) → (((A → B) → (C → (A → B))) → ((A → B) → ((C → A) → (C → B)))) [Chain]
3: ((C → (A → B)) → ((C → A) → (C → B))) → ((A → B) → ((C → (A → B)) → ((C → A) → (C → B)))) [Verum Ex]
4: (C → (A → B)) → ((C → A) → (C → B)) [Chain]
5: (A → B) → ((C → (A → B)) → ((C → A) → (C → B))) [MP 3, 4]
6: ((A → B) → (C → (A → B))) → ((A → B) → ((C → A) → (C → B))) [MP 2, 5]
7: ((A → B) → ((A → B) → (C → (A → B)))) → (((A → B) → (A → B)) → ((A → B) → (C → (A → B)))) [Chain]
8: ((A → B) → (C → (A → B))) → ((A → B) → ((A → B) → (C → (A → B)))) [Verum Ex]
9: (A → B) → (C → (A → B)) [Verum Ex]
10: (A → B) → ((A → B) → (C → (A → B))) [MP 8, 9]
11: ((A → B) → (A → B)) → ((A → B) → (C → (A → B))) [MP 7, 10]
12: (A → B) → (A → B) [Identity]
13: (A → B) → (C → (A → B)) [MP 11, 12]
14: (A → B) → ((C → A) → (C → B)) [MP 6, 13]
15: ((A → B) → (C → A)) → ((A → B) → (C → B)) [MP 1, 14]

Lemma 2: A weakened form of Ex Falso:
1: (A → ((B → ⊥) → (B → C))) → ((A → (B → ⊥)) → (A → (B → C))) [Chain]
2: ((B → ⊥) → (B → C)) → (A → ((B → ⊥) → (B → C))) [Verum Ex]
3: (B → (⊥ → C)) → ((B → ⊥) → (B → C)) [Chain]
4: (⊥ → C) → (B → (⊥ → C)) [Verum Ex]
5: ⊥ → C [Ex Falso]
6: B → (⊥ → C) [MP 4, 5]
7: (B → ⊥) → (B → C) [MP 3, 6]
8: A → ((B → ⊥) → (B → C)) [MP 2, 7]
9: (A → (B → ⊥)) → (A → (B → C)) [MP 1, 8]

Final Proof:
1: (((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A)) → ((((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) → (((A → (B → ⊥)) → ⊥) → A)) [Chain]
2: (((A → ⊥) → A) → A) → (((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A)) [Verum Ex]
3: ((A → ⊥) → A) → A [Mirabilis]
4: ((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A) [MP 2, 3]
5: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) → (((A → (B → ⊥)) → ⊥) → A) [MP 1, 4]
6: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥)) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) [Lemma 2]
7: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥)))) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥)) [Lemma 1]
8: ((A → ⊥) → (A → (B → ⊥))) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥)))) [Verum Ex]
9: ((A → ⊥) → (A → ⊥)) → ((A → ⊥) → (A → (B → ⊥))) [Lemma 2]
10: ((A → ⊥) → (A → A)) → ((A → ⊥) → (A → ⊥)) [Lemma 1]
11: (A → A) → ((A → ⊥) → (A → A)) [Verum Ex]
12: A → A [Identity]
13: (A → ⊥) → (A → A) [MP 11, 12]
14: (A → ⊥) → (A → ⊥) [MP 10, 13]
15: (A → ⊥) → (A → (B → ⊥)) [MP 9, 14]
16: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥))) [MP 8, 15]
17: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥) [MP 7, 16]
18: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A) [MP 6, 17]
19: ((A → (B → ⊥)) → ⊥) → A [MP 5, 18]

Quite a long proof!

Bye

Which specific Hilbert system? There are tons.
Probably the best way is to find a proof in a sequent calculus and convert it to the Hilbert system.

I use Polish notation.

Since you referenced the Wikipedia, we'll suppose our basis is

1 CpCqp.

2 CCpCqrCCpqCpr.

3 CCNpNqCqp.

We want to prove

NCaNb |- a.

I use the theorem prover Prover9. So, we'll need to parenthesize everything. Also, the variables of Prover9 go (x, y, z, u, w, v5, v6, ..., vn). All other symbols get interpreted as functions or relations or predicates. All axioms need a predicate symbol "P" before them also, which we can think of as meaning "it is provable that..." or more simply "provable". And all sentences in Prover9 need to get ended by a period. Thus, axioms 1, 2, and 3 become respectively:

1 P(C(x,C(y,x))).

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

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

We can combine the rules of uniform substitution and detachment into the rule of condensed detachment. In Prover9 we can represent this as:

-P(C(x,y)) | -P(x) | P(y).

The "|" indicates logical disjunction, and "-" indicates negation. Prover9 proves by contradiction. The rule says in words can get interpreted as saying "either it is not the case that if x, then y is provable, or it is not the case that x is provable, or y is provable." Thus, if it does hold that if x, then y is provable, the first disjunct fails. If it does hold that x is provable, then the second disjunct fails. So, if, if x, then y is provable, if x is provable, then the third disjunct, that y is provable follows by the rule.

Now we can't make substitutions in NCaNb, since it's not a tautology. Nor is "a". Thus, if we put

P(N(C(a,N(b)))).

as an assumption, Prover9 will interpret "a" and "b" as nullary functions, which effectively turns them into constants. We also want to make P(a) as our goal.

Now we can also "tune" Prover9 using various theorem-proving strategies such as weighting, resonance, subformula, pick-given ratio, level saturation (or even invent our own). I'll use the hints strategy a little bit, by making all of the assumptions (including the rule of inference), and the goal into hints. I'll also turn the max weight down to 40, and make 5 the number of maximum variables.

I use the version with the graphical interface, but here's the entire input:

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
assign(max_seconds, -1).
assign(max_weight, 40).
end_if.

if(Mace4).   % Options for Mace4
assign(max_seconds, 60).
end_if.

if(Prover9). % Additional input for Prover9
formulas(hints).
-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).
P(a).
end_of_list.
assign(max_vars,5).
end_if.

formulas(assumptions).

-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).

end_of_list.

formulas(goals).

P(a).

end_of_list.

Here's the proof it gave me:

============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 1312 was started by Doug on Machina2,
Mon Jun  9 22:35:37 2014
The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace43/bin-win32/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.01) seconds.
% Length of proof is 23.
% Level of proof is 9.
% Maximum clause weight is 20.
% Given clauses 49.

1 P(a) # label(non_clause) # label(goal).  [goal].
2 -P(C(x,y)) | -P(x) | P(y).  [assumption].
3 P(C(x,C(y,x))).  [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).  [assumption].
5 P(C(C(N(x),N(y)),C(y,x))).  [assumption].
6 P(N(C(a,N(b)))).  [assumption].
7 -P(a).  [deny(1)].
8 P(C(x,C(y,C(z,y)))).  [hyper(2,a,3,a,b,3,a)].
9 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).  [hyper(2,a,4,a,b,4,a)].
12 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))).  [hyper(2,a,4,a,b,5,a)].
13 P(C(x,C(C(N(y),N(z)),C(z,y)))).  [hyper(2,a,3,a,b,5,a)].
14 P(C(x,N(C(a,N(b))))).  [hyper(2,a,3,a,b,6,a)].
23 P(C(C(a,N(b)),x)).  [hyper(2,a,5,a,b,14,a)].
28 P(C(C(x,C(C(y,x),z)),C(x,z))).  [hyper(2,a,9,a,b,8,a)].
30 P(C(x,C(C(a,N(b)),y))).  [hyper(2,a,3,a,b,23,a)].
33 P(C(C(x,C(a,N(b))),C(x,y))).  [hyper(2,a,4,a,b,30,a)].
103 P(C(N(b),x)).  [hyper(2,a,33,a,b,3,a)].
107 P(C(x,b)).  [hyper(2,a,5,a,b,103,a)].
113 P(C(C(N(x),N(b)),x)).  [hyper(2,a,12,a,b,107,a)].
205 P(C(N(x),C(x,y))).  [hyper(2,a,28,a,b,13,a)].
209 P(C(N(a),x)).  [hyper(2,a,33,a,b,205,a)].
213 P(a).  [hyper(2,a,113,a,b,209,a)].
214 $F.  [resolve(213,a,7,a)].

============================== end of proof ==========================

라이센스 : CC-BY-SA ~와 함께 속성

제휴하지 않습니다 StackOverflow