Discussion:
Refuting Incompleteness and Undefinability Version(16) (fully parsed XML)
Add Reply
peteolcott
2018-11-07 05:24:26 UTC
Reply
Permalink
∀F ∈ Formal_Systems (~∃G ∈ L(F) (G ↔ ~(F ⊢ G)))

The fully operational parser actually parsed the following
expression into the XML that follows it below:
X @ ∀F ∈ Formal_Systems (~∃G ∈ F (G ↔ ~(F ⊢ G)))

LHS @ RHS provides a simple way to specify HOL expressions using
FOPL syntax. Whenever an expression refers to a LHS the parser
expands this into the full RHS, thus providing a simple means
to quantify over arbitrary levels of logic using FOPL syntax.

I think that I will revert back to Jim's suggestion and use the
"@" symbol to specify the <alias name> operator. I had switched
to "≡" for a while because it looked nicer. Jim pointed out
(to avoid confusion) that I should use something that does not
already have any conventional use in symbolic logic.

There is a slight nuance of a difference between the version(16)
expression and the following expression, the syntax recommended
by the world class expert could not yet be parsed into XML.

(world class expert)
We need to distinguish the language of formal system L(F) and
the formal system F (often equated with the set of its theorems).
Distinct systems may share the same language.

To fully define the language of my Version(16) expression would
require me to slightly adapt the current Backus–Naur form (BNF)
to parse the expression at the top of this posting.

I just used the term {language} as a term of the art of computer
science. If we use the term {language} as a term of the art of
symbolic logic this usage may vary. I am totally unaware of any
nuanced differences that may exist.

In any case I have now provided evidence (the BNF would be proof)
that have defined BNF that accepts WFF(F) and rejects ~WFF(F).

X @ ∀F ∈ Formal_Systems (~∃G ∈ F (G ↔ ~(F ⊢ G)))

<external_declaration_7>
<named_sentence_4 token="IDENTIFIER" value="X">
<sentence_21>
<quantified_variable_13 token="FOR_ALL">
<declare_type_8 token="ELEMENT_OF">
<declare_type_8 token="IDENTIFIER" value="F"/>
<declare_type_8 token="IDENTIFIER" value="Formal_Systems"/>
</declare_type_8>
</quantified_variable_13>
<sentence_23>
<sentence_22 token="NOT">
<sentence_21>
<quantified_variable_12 token="THERE_EXISTS">
<declare_type_8 token="ELEMENT_OF">
<declare_type_8 token="IDENTIFIER" value="G"/>
<declare_type_8 token="IDENTIFIER" value="F"/>
</declare_type_8>
</quantified_variable_12>
<sentence_23>
<sentence_17 token="IFF">
<atomic_sentence_25 token="IDENTIFIER" value="G"/>
<sentence_22 token="NOT">
<sentence_23>
<sentence_20 token="PROVES">
<atomic_sentence_25 token="IDENTIFIER" value="F"/>
<atomic_sentence_25 token="IDENTIFIER" value="G"/>
</sentence_20>
</sentence_23>
</sentence_22>
</sentence_17>
</sentence_23>
</sentence_21>
</sentence_22>
</sentence_23>
</sentence_21>
</named_sentence_4>
</external_declaration_7>


Copyright 2017 2018 Pete Olcott
peteolcott
2018-11-07 06:14:08 UTC
Reply
Permalink
Post by peteolcott
∀F ∈ Formal_Systems (~∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
The fully operational parser
You're a lying shitgibbon. Your "parser" is not "fully operational".
EFQ
The first page YACC BNF is very nearly the same as what my parser used:
https://www.researchgate.net/publication/317953772_Provability_with_Minimal_Type_Theory
Franz Gnaedinger
2018-11-07 07:05:04 UTC
Reply
Permalink
Post by peteolcott
Copyright 2017 2018 Pete Olcott
Peter Olcott holds a copyright on the following claims he made in sci.lang:
he knows the absolute and complete and total truth, he is the author of life
and creator of life, he has hundred reasons to believe that he is God, he
creates our future minds in order that we can go on existing, he is a human
being and God in personal union, he is the one Creator of the Universe.
Loading...