FOPL syntax of Minimal Type Theory (MTT)

<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
First Order Predicate Logic Syntax used as the basis for the
Minimal Type Theory Language: 
 
sentence 
 : atomic_sentence 
 | sentence IMPLIES sentence 
 | sentence IFF sentence 
 | sentence AND sentence 
 | sentence OR sentence 
 | sentence PROVES sentence // enhancement 
 | quantifier IDENTIFIER sentence // MTT syntax is
different 
 | '~' sentence %prec NOT 
 | '(' sentence ')' 
 ; 
 
atomic_sentence 
 : IDENTIFIER '(' term_list ')' // ATOMIC PREDICATE 
 | IDENTIFIER // SENTENTIAL
VARIABLE (enhancement) 
 ; 
 
term 
 : IDENTIFIER '(' term_list ')' // FUNCTION 
 | IDENTIFIER // CONSTANT or
VARIABLE 
 ; 
 
term_list 
 : term_list ',' term 
 | term 
 ; 
 
quantifier 
 : THERE_EXISTS 
 | FOR_ALL 
 ; 
 
</body>
</html>

DKleinecke

2017-07-01 17:46:05 UTC

Post by Pete Olcott
First Order Predicate Logic Syntax used as the basis for the
Minimal Type Theory Language:
sentence
        : atomic_sentence
        | sentence IMPLIES sentence
        | sentence IFF sentence
        | sentence AND sentence
        | sentence OR sentence
        | sentence PROVES sentence        // enhancement
        | quantifier IDENTIFIER sentence // MTT syntax is
different
        | '~' sentence %prec NOT
        | '(' sentence ')'
        ;

atomic_sentence
        : IDENTIFIER '(' term_list ')' // ATOMIC PREDICATE
        | IDENTIFIER                    // SENTENTIAL
VARIABLE (enhancement)
        ;

term
        : IDENTIFIER '(' term_list ')' // FUNCTION
        | IDENTIFIER                      // CONSTANT or
VARIABLE
        ;

term_list
        : term_list ',' term
        | term
        ;

quantifier
        : THERE_EXISTS
        | FOR_ALL
        ;

Is "%prec" perhaps a typo for '//'?

DKleinecke

2017-07-01 17:50:48 UTC

AS stated there must be at least one term in a term-list.
Hence
IDENTIFIER ( )
is not allowed. If it were

Pete Olcott

2017-07-01 18:13:05 UTC

Post by Pete Olcott
First Order Predicate Logic Syntax used as the basis for the
sentence
: atomic_sentence
| sentence IMPLIES sentence
| sentence IFF sentence
| sentence AND sentence
| sentence OR sentence
| sentence PROVES sentence // enhancement
| quantifier IDENTIFIER sentence // MTT syntax is
different
| '~' sentence %prec NOT
| '(' sentence ')'
;
atomic_sentence
: IDENTIFIER '(' term_list ')' // ATOMIC PREDICATE
| IDENTIFIER // SENTENTIAL
VARIABLE (enhancement)
;
term
: IDENTIFIER '(' term_list ')' // FUNCTION
| IDENTIFIER // CONSTANT or
VARIABLE
;
term_list
: term_list ',' term
| term
;
quantifier
: THERE_EXISTS
| FOR_ALL
;

AS stated there must be at least one term in a term-list.
Hence
IDENTIFIER ( )
is not allowed. If it were allowed would it differ from bare
IDENTIFIER ?

It parses correctly therefore it is correct. You just don't know YACC.

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

DKleinecke

2017-07-01 20:33:52 UTC

AS stated there must be at least one term in a term-list.
Hence
IDENTIFIER ( )
is not allowed. If it were allowed would it differ from bare
IDENTIFIER ?

It parses correctly therefore it is correct. You just don't know YACC.

I admit to not knowing much about and never using YACC but
do you mean by the first "It" IDENTIFIER ()? If your YACC
accepts that under your given BNF then your YACC is broken.

Pete Olcott

2017-07-01 22:04:38 UTC

AS stated there must be at least one term in a term-list.
Hence
IDENTIFIER ( )
is not allowed. If it were allowed would it differ from bare
IDENTIFIER ?

It parses correctly therefore it is correct. You just don't know YACC.

I admit to not knowing much about and never using YACC but
do you mean by the first "It" IDENTIFIER ()? If your YACC
accepts that under your given BNF then your YACC is broken.

https://groups.google.com/forum/#!original/comp.compilers/Qalayu9h3xw/gaTrXbbRd7AJ
Here is the original unmodified source on a newsgroup moderated by the famous author of a book about YACC and LEX.

If it was wrong he would have said something. Besides that YACC itself is smart enough to report all errors.

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

Pete Olcott

2017-07-01 18:11:31 UTC

Is "%prec" perhaps a typo for '//'?
If not what does it signify?

Precedence in YACC. The above grammar is the verbatim YACC BNF specification for the FOPL subset of MTT.

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

DKleinecke

2017-07-01 20:48:51 UTC

Is "%prec" perhaps a typo for '//'?
If not what does it signify?

Precedence in YACC. The above grammar is the verbatim YACC BNF specification for the FOPL subset of MTT.

I see. You left out the declarations part where NOT must turn
up and here you are stating that '~' has the same precedence
as NOT. But it seems to me that NOT is never generated by your
rules. Yet you say YACC accepts this. I wonder.

Pete Olcott

2017-07-01 22:08:07 UTC

Is "%prec" perhaps a typo for '//'?
If not what does it signify?

Precedence in YACC. The above grammar is the verbatim YACC BNF specification for the FOPL subset of MTT.

I left out everything besides the unequivocal proof that MTT really is fundamentally based on FOPL syntax.

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

Peter Percival

2017-07-01 23:15:23 UTC