Transforming formal proof into sound deduction (greatly simplified)

[PeteOlcott]

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.

[Logik]

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:

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]

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:

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
else is already done.

[Logik]

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
else is already done.

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]

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
else is already done.

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.

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
else is already done.

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]

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".

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]

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".

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]

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?

[PeteOlcott]

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]

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.

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]

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]

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]

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]

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]

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