Discussion:
Minimal Type Theory is derived by slightly augmenting FOPL syntax
(too old to reply)
Pete Olcott
2017-12-25 18:09:05 UTC
Permalink
<html>
<head>

<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
By adding a single &lt;assign alias&gt; operator to the syntax of
FOPL and generalizing the specialized identifier names, (shown in
the BNF below) Minimal Type Theory specifies any Higher Order Logic
expression using syntax nearly identical First Order Predicate
Logic. <br>
<br>
<a class="moz-txt-link-freetext" href="http://www.cyc.com/documentation/ontologists-handbook/writing-efficient-cycl/cycl-representation-choices/">http://www.cyc.com/documentation/ontologists-handbook/writing-efficient-cycl/cycl-representation-choices/</a><br>
Minimal Type Theory can specify Davidsonian Representations in a
hierarchy of unlimited finite depth. <br> <br> <b>The syntax of FOPL is extended by adding an &lt;assign alias&gt;
operator:</b><b><br>
</b>LHS is assigned as an alias name for the RHS<br>
<b>LHS ≡ RHS</b><b><br>
</b>The LHS is logically equivalent to the RHS Because the LHS is
merely an alias name for the RHS<br>
<br>
The biconditional ↔ retains its original semantic meaning referenced
in the BNF (shown below) as IFF <br>
<br>
These specialized identifier names: {PREDICATE, FUNCTION,  CONSTANT,
VARIABLE} are generalized into a single lexical token: IDENTIFIER <br>
<br>
<b>Copyright 2017 Pete Olcott </b><b><br>
</b><br>
<a class="moz-txt-link-freetext" href="https://groups.google.com/forum/#!msg/comp.compilers/Qalayu9h3xw/gaTrXbbRd7AJ">https://groups.google.com/forum/#!msg/comp.compilers/Qalayu9h3xw/gaTrXbbRd7AJ</a>
<br>
<b>YACC BNF syntax of First Order Predicate Logic (from above link)</b><b><br>
</b><br>
sentence<br>
        : atomic_sentence<br>
        | sentence IMPLIES sentence<br>
        | sentence IFF sentence<br>
        | sentence AND sentence<br>
        | sentence OR sentence<br>
        | quantifier VARIABLE sentence<br>
        | '~' sentence %prec NOT<br>
        | '(' sentence ')'<br>
        ;<br>
atomic_sentence<br>
        : PREDICATE '(' term_list ')'<br>
        | term '=' term<br>
        ;<br>
term<br>
        : FUNCTION '(' term_list ')'<br>
        | CONSTANT<br>
        | VARIABLE<br>
        ;<br>
term_list<br>
        : term_list term<br>
        | term<br>
        ;<br>
quantifier<br>
        : THERE_EXISTS<br>
        | FORALL<br>
        ;<br>
<br>
<div class="moz-signature">-- <br>
<meta charset="UTF-8">
        <b>Γ ⊢<sub><font style="font-size: 8pt" size="1">FS</font></sub>
A ≡ ∃Γ ⊆ FS Provable(Γ, A)</b> // MTT notational conventions<br>
<b>∀X True(X) ≡ ∃Γ ⊆ MTT ∧ Axioms(Γ) Provable(Γ, X) </b> // MTT
Truth Predicate </div>
</body>
</html>
Mścisław Wojna-Bojewski
2017-12-30 22:31:10 UTC
Permalink
By adding a single <assign alias> operator to the syntax of
FOPL and generalizing the specialized identifier names, (shown in
the BNF below) Minimal Type Theory specifies any Higher Order Logic
expression using syntax nearly identical First Order Predicate
Logic.
http://www.cyc.com/documentation/ontologists-handbook/writing-efficient-cycl/cycl-representation-choices/
Minimal Type Theory can specify Davidsonian Representations in a
hierarchy of unlimited finite depth.
The syntax of FOPL is extended by adding an <assign alias>
LHS is assigned as an alias name for the RHS
LHS ≡ RHS
The LHS is logically equivalent to the RHS Because the LHS is
merely an alias name for the RHS
The biconditional ↔ retains its original semantic meaning referenced
in the BNF (shown below) as IFF
These specialized identifier names: {PREDICATE, FUNCTION,  CONSTANT,
VARIABLE} are generalized into a single lexical token: IDENTIFIER
Copyright 2017 Pete Olcott
https://groups.google.com/forum/#!msg/comp.compilers/Qalayu9h3xw/gaTrXbbRd7AJ
YACC BNF syntax of First Order Predicate Logic (from above link)
sentence
        : atomic_sentence
        | sentence IMPLIES sentence
        | sentence IFF sentence
        | sentence AND sentence
        | sentence OR sentence
        | quantifier VARIABLE sentence
        | '~' sentence %prec NOT
        | '(' sentence ')'
        ;
atomic_sentence
        : PREDICATE '(' term_list ')'
        | term '=' term
        ;
term
        : FUNCTION '(' term_list ')'
        | CONSTANT
        | VARIABLE
        ;
term_list
        : term_list term
        | term
        ;
quantifier
        : THERE_EXISTS
        | FORALL
        ;
--
        Γ ⊢FS
A ≡ ∃Γ ⊆ FS Provable(Γ, A) // MTT notational conventions
∀X True(X) ≡ ∃Γ ⊆ MTT ∧ Axioms(Γ) Provable(Γ, X) // MTT
Truth Predicate
Not related to linguistics or languages. Completely irrelevant.

Loading...