## Transforming formal proof into sound deduction (greatly simplified)

What is the basis for reason? And mathematics?

Moderators: AMod, iMod

PeteOlcott
Posts: 875
Joined: Mon Jul 25, 2016 6:55 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

Logik wrote:
Thu Apr 25, 2019 7:30 pm
PeteOlcott wrote:
Thu Apr 25, 2019 7:13 pm
Axiom(0) Stipulates** this definition of Axiom:
Expressions of language defined to have the semantic value of Boolean True.
Provides the symbolic logic equivalent of true premises.

Stipulating** this specification of True and False: (TRUE ↔ ⊤ ∧ FALSE ↔ ⊥)
Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
Thus stipulating** that consequences are provable from axioms.

Stipulating** that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
Screens out semantically unsound sentences as not belonging to the formal system.
Also. I can't parse any of that. It's in some made up language that I don't care to learn.

Write it in C++.

I am most interested in these functions:

True()
False()
Closed_WFF()
↔()
∈()
There are millions of lines that support those functions.

The exact same thing can be explained in terms of a Prolog query.
A Prolog query returns: "Yes" for True
and "Yes" for the negation of the query for False.
Everything else is unsound.

Prolog would say: "No"
there are statements of the language of F which can neither be proved nor disproved in F. (Raatikainen 2018)
Thus refuting the 1931 Incompleteness Theorem.

Prolog would say: "No"
(3) x ∉ Pr if and only if x ∈ Tr
Because in Prolog ONLY Provable means True.
Thus refuting the Tarski Undefinability Theorem.
Last edited by PeteOlcott on Thu Apr 25, 2019 7:49 pm, edited 1 time in total.

Logik
Posts: 4041
Joined: Tue Dec 04, 2018 12:48 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

PeteOlcott wrote:
Thu Apr 25, 2019 7:45 pm
There are millions of lines that support those functions.

The exact same thing can be explained in terms of a Prolog query.
A Prolog query returns: "Yes" for True
and "Yes" for the negation of the query for False.
Everything else is unsound.
Very well, so you will be prodicing the Prolog code which proves your sound deductive claim when?

I am referring to this sound deduction in particular:
PeteOlcott wrote:
Thu Apr 25, 2019 7:13 pm
You are using the wrong meaning of synthetic.
I want to see the Prolog query which returns TRUE when I am using the correct meaning of "synthetic"; and returns FALSE when I am using the incorrect meaning of "synthetic".

PeteOlcott
Posts: 875
Joined: Mon Jul 25, 2016 6:55 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

Logik wrote:
Thu Apr 25, 2019 7:48 pm
PeteOlcott wrote:
Thu Apr 25, 2019 7:45 pm
There are millions of lines that support those functions.

The exact same thing can be explained in terms of a Prolog query.
A Prolog query returns: "Yes" for True
and "Yes" for the negation of the query for False.
Everything else is unsound.
Very well, so you will be prodicing the Prolog code which proves your sound deductive claim when?

I am referring to this claim in particular:
PeteOlcott wrote:
Thu Apr 25, 2019 7:13 pm
You are using the wrong meaning of synthetic.
I want to see the Prolog query which returns TRUE when I am using the correct meaning of "synthetic"; and returns FALSE when I am using the incorrect meaning of "synthetic".
The inherent design of Prolog already provides the sound deductive inference model
and the sound deductive inference model already refutes Tarski and Gödel.

All that I have to actually produce is the explanation of why this is true. Everything

Logik
Posts: 4041
Joined: Tue Dec 04, 2018 12:48 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

PeteOlcott wrote:
Thu Apr 25, 2019 7:53 pm
The inherent design of Prolog already provides the sound deductive inference model
and the sound deductive inference model already refutes Tarski and Gödel.

All that I have to actually produce is the explanation of why this is true. Everything
If everything else is already done, I trust the algorithm will be provided shortly?

How long do you need? 15 minutes?

If Tarski and Gödel are refuted then your system is consistent and complete and you shall have absolutely no problem doing what I am asking you to do.

PeteOlcott
Posts: 875
Joined: Mon Jul 25, 2016 6:55 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

Logik wrote:
Thu Apr 25, 2019 7:53 pm
PeteOlcott wrote:
Thu Apr 25, 2019 7:53 pm
The inherent design of Prolog already provides the sound deductive inference model
and the sound deductive inference model already refutes Tarski and Gödel.

All that I have to actually produce is the explanation of why this is true. Everything
If everything else is already done, I trust the algorithm will be provided shortly?

How long do you need? 15 minutes?

If Tarski and Gödel are refuted then your system is consistent and complete and you shall have absolutely no problem doing what I am asking you to do.
Logik wrote:
Thu Apr 25, 2019 7:53 pm
PeteOlcott wrote:
Thu Apr 25, 2019 7:53 pm
The inherent design of Prolog already provides the sound deductive inference model
and the sound deductive inference model already refutes Tarski and Gödel.

All that I have to actually produce is the explanation of why this is true. Everything
If everything else is already done, I trust the algorithm will be provided shortly?

How long do you need? 15 minutes?

If Tarski and Gödel are refuted then your system is consistent and complete and you shall have absolutely no problem doing what I am asking you to do.
Prolog already exists and because It implements the sound deductive inference
model Prolog <IS> the algorithm.

I ONLY have to show that examining Tarski and Gödel within this model
refutes both of them. Anyone knowing symbolic logic will be able to verify
that based on my paper.

Since Prolog already KNOWS that Provable and True are the same thing
there is no way in Prolog to express any discrepancy of this.

If you ask it to determine is unprovability is provable it fails a unify on
occurs check/2, meaning that you specified an infinite loop.

Logik
Posts: 4041
Joined: Tue Dec 04, 2018 12:48 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

PeteOlcott wrote:
Thu Apr 25, 2019 8:11 pm
Prolog already exists and because It implements the sound deductive inference
model Prolog <IS> the algorithm.
No. Prolog is a system, not an algorithm.

I am asking you to show us the deductive steps through which you deduced that I am using the the wrong meaning of "synthetic".

PeteOlcott wrote:
Thu Apr 25, 2019 8:11 pm
I ONLY have to show that examining Tarski and Gödel within this model
refutes both of them. Anyone knowing symbolic logic will be able to verify
that based on my paper.
How have you deduced/verified/proven that you know symbolic logic?

PeteOlcott
Posts: 875
Joined: Mon Jul 25, 2016 6:55 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

Logik wrote:
Thu Apr 25, 2019 8:14 pm
PeteOlcott wrote:
Thu Apr 25, 2019 8:11 pm
Prolog already exists and because It implements the sound deductive inference
model Prolog <IS> the algorithm.
No. Prolog is a system, not an algorithm.

I am asking you to show us the deductive steps through which you deduced that I am using the the wrong meaning of "synthetic".

PeteOlcott wrote:
Thu Apr 25, 2019 8:11 pm
I ONLY have to show that examining Tarski and Gödel within this model
refutes both of them. Anyone knowing symbolic logic will be able to verify
that based on my paper.
How have you deduced/verified/proven that you know symbolic logic?
This is becoming pointless.

Logik
Posts: 4041
Joined: Tue Dec 04, 2018 12:48 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

PeteOlcott wrote:
Thu Apr 25, 2019 8:40 pm
This is becoming pointless.
Is that your way of saying that you can't express your own sound, deductive reasoning, despite having a complete, consistent and decidable logic-system at your disposal?
Last edited by Logik on Thu Apr 25, 2019 8:49 pm, edited 1 time in total.

PeteOlcott
Posts: 875
Joined: Mon Jul 25, 2016 6:55 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

Logik wrote:
Thu Apr 25, 2019 8:41 pm
PeteOlcott wrote:
Thu Apr 25, 2019 8:40 pm
This is becoming pointless.
Is that your way of saying that you can't express your own sound, deductive reasoning, despite having a complete, consistent and decidable logic-system at your disposal?
I cannot explain the key point of how I converted formal proofs of symbolic logic
to conform to the sound deductive inference model to people that don't know symbolic logic.

When I explain the analogy to Prolog they are stuck in rebuttal mode grasping at straws
to form some kind of rebuttal when no sound basis for any rebuttal actually exists.

Logik
Posts: 4041
Joined: Tue Dec 04, 2018 12:48 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

PeteOlcott wrote:
Thu Apr 25, 2019 8:49 pm
I cannot explain the key point of how I converted formal proofs of symbolic logic
to conform to the sound deductive inference model to people that don't know symbolic logic.
But you can explain it to yourself, can you not? And you understand symbolic logic.

So... go ahead and provide the deductive proof for "Pete Olcott knows symbolic logic" in symbolic logic. Or Prolog.

PeteOlcott wrote:
Thu Apr 25, 2019 8:49 pm
When I explain the analogy to Prolog they are stuck in rebuttal mode grasping at straws
to form some kind of rebuttal when no sound basis for any rebuttal actually exists.
Naturally. You are unable to recognize why it's a valid rebuttal because you don't understand symbolic logic or symbol manipulation.

Speakpigeon
Posts: 964
Joined: Sat Nov 11, 2017 3:20 pm
Location: Paris, France, EU

### Re: Transforming formal proof into sound deduction (greatly simplified)

I don't see what would be the use or consequences of proving current first order logic wrong. Specifically, I'm not sure how the so-called principle of explosion affects or could possibly affect mathematical theorems. Gödel maybe?
EB

Logik
Posts: 4041
Joined: Tue Dec 04, 2018 12:48 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

Speakpigeon wrote:
Tue Apr 30, 2019 5:50 pm
I'm not sure how the so-called principle of explosion affects or could possibly affect mathematical theorems. Gödel maybe?
EB
It affects all formal systems. From a contradiction anything follows, which trivialises the notions of truth and falsity.

https://en.wikipedia.org/wiki/Principle_of_explosion

So you have a choice. Either make the formal system absolutely perfect (eliminate ALL things which cause contradictions - e.g grammatical, syntactic and semantic errors) or deal with the contradictions as they arise.

Speakpigeon
Posts: 964
Joined: Sat Nov 11, 2017 3:20 pm
Location: Paris, France, EU

### Re: Transforming formal proof into sound deduction (greatly simplified)

Logik wrote:
Tue Apr 30, 2019 6:03 pm
Speakpigeon wrote:
Tue Apr 30, 2019 5:50 pm
I'm not sure how the so-called principle of explosion affects or could possibly affect mathematical theorems. Gödel maybe?
EB
It affects all formal systems. From a contradiction anything follows, which trivialises the notions of truth and falsity.

https://en.wikipedia.org/wiki/Principle_of_explosion

So you have a choice. Either make the formal system absolutely perfect (eliminate ALL things which cause contradictions - e.g grammatical, syntactic and semantic errors) or deal with the contradictions as they arise.
So, how does that affect mathematical theorems at all?
EB

Logik
Posts: 4041
Joined: Tue Dec 04, 2018 12:48 pm

### Re: Transforming formal proof into sound deduction (greatly simplified)

Speakpigeon wrote:
Wed May 01, 2019 12:25 pm
Logik wrote:
Tue Apr 30, 2019 6:03 pm
Speakpigeon wrote:
Tue Apr 30, 2019 5:50 pm
I'm not sure how the so-called principle of explosion affects or could possibly affect mathematical theorems. Gödel maybe?
EB
It affects all formal systems. From a contradiction anything follows, which trivialises the notions of truth and falsity.

https://en.wikipedia.org/wiki/Principle_of_explosion

So you have a choice. Either make the formal system absolutely perfect (eliminate ALL things which cause contradictions - e.g grammatical, syntactic and semantic errors) or deal with the contradictions as they arise.
So, how does that affect mathematical theorems at all?
EB
Mathematicians typically go for the first strategy. Ideal. Perfection. Beauty.

Best of luck to them.

Speakpigeon
Posts: 964
Joined: Sat Nov 11, 2017 3:20 pm
Location: Paris, France, EU

### Re: Transforming formal proof into sound deduction (greatly simplified)

Logik wrote:
Wed May 01, 2019 12:28 pm
Speakpigeon wrote:
Wed May 01, 2019 12:25 pm
So, how does that affect mathematical theorems at all?
Mathematicians typically go for the first strategy. Ideal. Perfection. Beauty.
In this case, no.
Mathematicians settled for a logic that is less than ideal. They've shown themselves pragmatic and effective rather than idealist. Remember, it's Russell who managed the incident, and he really, really disliked idealism.
EB

### Who is online

Users browsing this forum: No registered users and 34 guests