There are millions of lines that support those functions.Logik wrote: ↑Thu Apr 25, 2019 7:30 pmAlso. I can't parse any of that. It's in some made up language that I don't care to learn.PeteOlcott wrote: ↑Thu Apr 25, 2019 7:13 pmAxiom(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.

Write it in C++.

I am most interested in these functions:

True()

False()

Closed_WFF()

↔()

∈()

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.