Pete Olcott

2017-06-17 16:48:54 UTC

"@" means the LHS is assigned as an alias for the RHS.

Thus the LHS nickname is to be considered one-and-the-same-thing as the expression on the RHS, as if macro substitution was to take place.

The primary purpose of this syntax is to provide the means for an expression to directly refer to itself. This is not at all the same convention that Tarski provided where a quoted expression is considered to be the name of the expression so that an expression can refer to its name.

With Tarski's convention the true nature of pathological self-reference cannot be expressed, it slips through the cracks of expressibility without ever being seen.

Provable(L, X) @ L ∈ Formal_Systems, ∃Γ ⊂ L (Γ ⊢ X)

~Provable(L, X) @ L ∈ Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ X)

~Provable(L, X) @ L ∈ Formal_Systems, ∀Γ ⊂ L ~(Γ ⊢ X)

Refutable(L, X) @ L ∈ Formal_Systems, ∃Γ ⊂ L (Γ ⊢ ~X)

We use: L ∈ Formal_Systems

instead of: ∃L ∈ Formal_Systems

because L ∈ Formal_Systems is an axiom and not an assertion, Formal_Systems is a predefined constant that is defined to have at least one element.

// Neither provable nor refutable in any formal system:

G @ ∀L ∈ Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ G)

Copyright 2017 Pete Olcott

Thus the LHS nickname is to be considered one-and-the-same-thing as the expression on the RHS, as if macro substitution was to take place.

The primary purpose of this syntax is to provide the means for an expression to directly refer to itself. This is not at all the same convention that Tarski provided where a quoted expression is considered to be the name of the expression so that an expression can refer to its name.

With Tarski's convention the true nature of pathological self-reference cannot be expressed, it slips through the cracks of expressibility without ever being seen.

Provable(L, X) @ L ∈ Formal_Systems, ∃Γ ⊂ L (Γ ⊢ X)

~Provable(L, X) @ L ∈ Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ X)

~Provable(L, X) @ L ∈ Formal_Systems, ∀Γ ⊂ L ~(Γ ⊢ X)

Refutable(L, X) @ L ∈ Formal_Systems, ∃Γ ⊂ L (Γ ⊢ ~X)

We use: L ∈ Formal_Systems

instead of: ∃L ∈ Formal_Systems

because L ∈ Formal_Systems is an axiom and not an assertion, Formal_Systems is a predefined constant that is defined to have at least one element.

// Neither provable nor refutable in any formal system:

G @ ∀L ∈ Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ G)

Copyright 2017 Pete Olcott

--

(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)

(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)