T: Is the Proof in Predicate Calculus Correct?

[solakis1]

Let :
1)P one place operation
.........m is a constant......
2)K one place operation

let :
1) G two place predicate
2) H two place predicate
Let :
The following axioms or assumptions)
1)for all A { H(A,m)v H(m,A)v G(A,m)}
2)for all A { H(A,m)=> G[P(A),A]}
3)for all A {H(m,A) => G[P(A),K(A)]}
4)for all A {G[K(A),m] => G(A,m)}.
5)for all A,B,C { [G(A,B) and G(A,C)]=> G(B,C)}
Then formally prove :
for all A {G[P(A),m] => G(A,m)}

 

[Evgeny.Makarov]

This problem has two parts: proving the claim informally and then translating the proof into a formal derivation. The second part depends on the formal system, i.e., the definition of a derivation. I have not though about this problem, but have you proved this statement on paper?

 

[solakis1]

This problem has two parts: proving the claim informally and then translating the proof into a formal derivation. The second part depends on the formal system, i.e., the definition of a derivation. I have not though about this problem, but have you proved this statement on paper?

No

How do we prove the statement informaly??

Do we have informal proofs in predicate calculus?

 

[Deveno]

start with axiom (1) (that looks the most promising). we can assume G(P(A),m).

if G(A,m) there's nothing to prove (note: it may "make more sense" to prove that if not H(A,m) and not H(m,A) then necessarily G(A,m), essentially "saving this case for last").

if H(A,m), then G(P(A),A) by (2), so we have G(A,m) by (3)

(since we have G(P(A),A) and G(P(A),m)).

if H(m,A), then we have G(A,m) by (3) and (4) and transitivity of implication.

i have no idea what i just proved, but I'm pretty sure i did it "informally".

 

[solakis1]

start with axiom (1) (that looks the most promising). we can assume G(P(A),m).

if G(A,m) there's nothing to prove (note: it may "make more sense" to prove that if not H(A,m) and not H(m,A) then necessarily G(A,m), essentially "saving this case for last").

if H(A,m), then G(P(A),A) by (2), so we have G(A,m) by (3)

(since we have G(P(A),A) and G(P(A),m)).

if H(m,A), then we have G(A,m) by (3) and (4) and transitivity of implication.

i have no idea what i just proved, but I'm pretty sure i did it "informally".

I wonder could that informal proof be checked thru a computer program??

 

[CaptainBlack]

I wonder could that informal proof be checked thru a computer program??

An informal proof is for the benefit of Humans who want to understand what is going on. An informal proof must be translated into a formal proof for machine verification (or translated from a formal to informal proof for the benefit of Humans if the proof is in fact machine generated).

CB

 

[Evgeny.Makarov]

I wonder could that informal proof be checked thru a computer program??

I indeed formalized this proof in Coq. Here is the script.

Parameters (T : Type) (m : T) (p k : T -> T) (G H : T -> T -> Prop).

Axiom a1 : forall A,  H A m \/ H m A \/ G A m.
Axiom a2 : forall A,  H A m-> G (p A) A.
Axiom a3 : forall A, H m A -> G (p A) (k A).
Axiom a4 : forall A, G (k A) m -> G A m.
Axiom a5 : forall A B C, G A B -> G A C-> G B C.

Theorem t : forall A, G (p A) m -> G A m.
Proof.
intros A P. (* assume A and P : G (p A) m *)
destruct (a1 A) as [? | [? | ?]].
(* Case when H A m *)
+ assert (G (p A) A) by (apply a2; trivial).
  eapply a5; eauto.
(* Case when H m A *)
+ assert (G (p A) (k A)) by (apply a3; trivial).
  assert (G (k A) m) by (eapply a5; eauto).
  apply a4; trivial.
(* Case when G A m *)
+ trivial.
Qed.

In fact, Coq is smart enough to prove most of the claim automatically:

Theorem t1 : forall A, G (p A) m -> G A m.
Proof.
intros; destruct (a1 A) as [? | [? | ?]]; eauto.
Qed.

Note that this is not a formal derivation; this is a script consisting of commands that generate a derivation. The derivation of t1 is

t1 = 
fun (A : T) (H0 : G (p A) m) =>
let o := a1 A in
match o with
| or_introl H1 => a5 (p A) A m (a2 A H1) H0
| or_intror (or_introl H2) => a4 A (a5 (p A) (k A) m (a3 A H2) H0)
| or_intror (or_intror H2) => H2
end

I don't expect anyone here to understand this, but if you want to try, disjunction is right-associative in Coq, so or_introl H1 is the case when H1 : H A m, or_intror (or_introl H2) is when H2 : H m A and or_intror (or_intror H2) is when H2 : G A m.

As I said in another thread, this derivation is also isomorphic to a derivation in natural deduction, so it can be straightforwardly translated, for example, into Fitch notation.

 

[solakis1]

An informal proof is for the benefit of Humans who want to understand what is going on. An informal proof must be translated into a formal proof for machine verification (or translated from a formal to informal proof for the benefit of Humans if the proof is in fact machine generated).

CB

Why,do you understand the informal proof Deveno wrote??

 

[CaptainBlack]

Why,do you understand the informal proof Deveno wrote??

That would require that I were interested enough in the original question to read the question and purported proof in detail. But I'm not, mainly because formal logics are of no intrinsic interest to me.

CB