MHB Prove the Validity of Euclid's Elements

[solakis1]

Let:

1) m be a constant

2) P ,K be one place operation symbols

3) F be two places operation symbol4) H,G be two places predicate symbols
Let, the following assumptions:1) $\forall A\forall B [ H(A,m)\Longrightarrow G[P(A),B]\Longleftrightarrow G[K(B),A]\wedge H(B,m)]$2) $\forall A\forall B[ H(A,m)\wedge H(B,m)\Longrightarrow H(F(A,B),m)]$

3)$\forall A\forall B\forall C\forall D[ G[A,B]\wedge G[C,D]\Longrightarrow G[F(A,C),F(B,D)]]$

4)$\forall A\forall B [ G[F(K(P(A)),K(P(B))),K(F(P(A),P(B)))]]$

5)$\forall A\forall B\forall C [ G[A,B]\wedge G[A,C]\Longrightarrow G[B,C]]$

6) $\forall A [ G(A,A) ]$

Then prove :

$\forall A\forall B [ H(A,m)\wedge H(B,m)\Longrightarrow G[ P(F(A,B)),F(P(A),P(B))]]$

 

[Evgeny.Makarov]

In premise (1), is it

H(A,m) => (G[P(A),B] <=> G[K(B),A] /\ H(B,m))

or

(H(A,m) => G[P(A),B]) <=> G[K(B),A] /\ H(B,m)?

Also, this is a metamathematical question, but why is this problem interesting? Without knowing the semantics of P, K, F, H and G, it's just some manipulation of symbols. I am not sure how it gives any additional insight into logic.

 

[solakis1]

In premise (1), is it

H(A,m) => (G[P(A),B] <=> G[K(B),A] /\ H(B,m))

or

(H(A,m) => G[P(A),B]) <=> G[K(B),A] /\ H(B,m)?

Also, this is a metamathematical question, but why is this problem interesting? Without knowing the semantics of P, K, F, H and G, it's just some manipulation of symbols. I am not sure how it gives any additional insight into logic.

It is : H(A,m) => (G[P(A),B] <=> G[K(B),A] /\ H(B,m))

Well is it not every mathematical proof a manipulation of symbols??

 

[CaptainBlack]

It is : H(A,m) => (G[P(A),B] <=> G[K(B),A] /\ H(B,m))

Well is it not every mathematical proof a manipulation of symbols??

Actually no, this is a fiction foisted on us by certain philosophies of mathematics.

A proof is an argument that convinces mathematicians. What counts as proof changes with time and context.

CB

 

[solakis1]

.

A proof is an argument that convinces mathematicians.

CB

How ??

 

[CaptainBlack]

How ??

How is anyone convinced of anything. Look at Euclid, it is full of "proofs" that were considered convincing for over 2000 years.

CB

 

[solakis1]

How is anyone convinced of anything.

Not of anything ,but of a mathematical argument.

Anyway that is what i asked you

Look at Euclid, it is full of "proofs" that were considered convincing for over 2000 years.

CB

Euclid along with his "elements " wrote a book called "Pseudaria".

The contents and the magnitude of its validity can be found in Proclus,p.70,1- 18

The book is considered to be the 1st proof checker in human history (at least for the Geometrical theorems,that is).

Unfortunately the book was irreparably lost.