Provability: ∃Γ ⊆ FS Provable(Γ, A)

[Pete Olcott]

https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence

A formula A is a syntactic consequence within some formal system 𝓕𝓢 of a set Γ of formulas if there is a formal
proof in 𝓕𝓢 of A from the set Γ.          Γ ⊢_𝓕𝓢 A    ≡   ∃Γ ⊆ FS Provable(Γ, A)

All sound inference begins with a set of finite string axioms and through a specific set of finite string transformation rules derives a finite string conclusion. This combines Aristotle and Hilbert.

Invalid reasoning (the whole set of fallacies) is using any finite string transformation rules that are not in the predefined set. © 2107 Pete Olcott

-- 
Defining Tarski’s ∀x True(x) ↔ φ(x) 
∀x True(x)  ↔ ∃y Provable(y, x)  // True entirely defined by Provability
∀x False(x) ↔ ∃y Provable(y, ~x) // False entirely defined by Refutability

[Pete Olcott]

On 12/2/2017 3:23 PM, Peter Percival wrote:

peteolcott wrote:

All sound inference begins with a set of finite string axioms and
through a specific set of finite string transformation rules
derives a finite string conclusion. This combines Aristotle and
Hilbert.

To me, a sound inference is one that transmits truth from the premises to the conclusion.  Your account is very vague: what axioms, what rules?  Mine is also problematic: what is truth?  (Of course, I don't mean "mine" literally, I am just quoting what I have learned.)  Can you give relevant citations for Aristotle and Hilbert?

Invalid reasoning (the whole set of fallacies) is using any finite
string transformation rules that are not in the predefined set.

There you go again, what set?

My intention is to shown that truth is consistently and completely defined by a set of axioms.
This post is a sketch of the outline of this proof, by setting the foundational ground rules.

Aristotle:
(1) True Premises
(2) Valid Deductive Logical Inference
(3) Sound Conclusion

Interpreting Aristotle in terms of Hilbert (© 2017 Pete Olcott)
(1) Finite String Axioms  // true premises
(2) Predefined set of Finite String Transformation Rules // valid inference
(3) Correct Finite String Conclusion  // sound conclusion

http://liarparadox.org/index.php/2017/11/03/refuting-the-conclusion-of-godels-1931-incompleteness-theorem/ 
 
Copyright 2017 Pete Olcott

[burs...@gmail.com]

Things like © 2107 Pete Olcott give indicative
of some serious mental problems...

Am Samstag, 2. Dezember 2017 17:19:04 UTC+1 schrieb Pete Olcott:

[Pete Olcott]

On 12/3/2017 10:48 AM, Rupert wrote:

Peter Olcott, from what you say here it would appear that you would like to give some kind of definition of truth. Truth in any particular language? First-order language of arithmetic?

First Order Languages artificially restrict their Relations to First Order objects. They cannot for example express Relations between Relations.

My own Minimal Type Theory is almost identical to FOL except that it can express Relations between (or among)  any element of the set of Things.

https://philpapers.org/archive/PETMTT-4.pdf
https://philpapers.org/archive/OLCPWM.pdf

My definition of Truth is in my signature line: 

[Pete Olcott]

On 12/3/2017 12:09 PM, Rupert wrote:

Well, you didn't answer my question...

Maybe my answer was not direct enough:
The WFF of my signature line defines Truth in Minimal Type Theory (and any analogous system) that can exhaustively define (every aspect of every) Relation between (or among) every element of the set of Things.

∀x True(x)  ↔ ∃y Provable(y, x)  // True entirely defined by Provability ---

Copyright 2017 Pete Olcott   // The above is brand new material that I have never said before.

[Pete Olcott]

∀x True(x) ↔ (∀L ∈ Formal_Systems ∃Γ ⊆ L Provable(Γ, x))

[Pete Olcott]

On 12/3/2017 1:23 PM, Rupert wrote:

Because you didn't answer. Yes, I know you think that's a definition of truth. Truth in which language? You didn't answer.

For the third time now: Truth in the language of Minimal Type Theory...

[Pete Olcott]

On 12/3/2017 10:48 AM, Rupert wrote:

On Saturday, December 2, 2017 at 11:21:28 PM UTC+1, Pete Olcott wrote:

Peter Olcott, from what you say here it would appear that you would like to give some kind of definition of truth. Truth in any particular language? First-order language of arithmetic?

This WFF defines Truth in the language of Minimal Type Theory
∀x True(x) ↔ (∃Γ ⊆ MTT Provable(Γ, x))

This WFF defines Truth in the language of Minimal Type Theory and every other language capable of expressing every Relation between (or among) every element of the set of Things.

∀x True(x) ↔ (∀L ∈ Formal_Systems ∃Γ ⊆ L Provable(Γ, x))

Since FOL cannot even express a Relation between Relations, I am definitely excluding FOL from consideration. 

[Pete Olcott]

On 12/4/2017 8:17 AM, Peter Percival wrote:

peteolcott wrote:

The expressions that I am using now seem to be conventional second or
third order logic. Thus their language is already defined.

That it only seems and that it's something or something else doesn't look promising.  But let's be positive and suppose that it's second order.  There is more than one second order language.  Which is yours? (If it turns out to be third order, a similar question arises.)  Once the language is fixed, there are such questions as do you have comprehension axioms?

https://en.wikipedia.org/wiki/Second-order_logic

First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations.

Second-order logic also includes quantification over sets, functions, and other variables as explained in the section Syntax and fragments.

Since my expression quantifies over set of relations (WFF) that would seem to make it 3rd Order Logic.

See next reply for more details:   Copyright 2017 Pete Olcott

[Pete Olcott]

On 12/4/2017 9:51 AM, Pete Olcott wrote:

On 12/4/2017 8:17 AM, Peter Percival wrote:

peteolcott wrote:

The expressions that I am using now seem to be conventional second or
third order logic. Thus their language is already defined.

That it only seems and that it's something or something else doesn't look promising.  But let's be positive and suppose that it's second order.  There is more than one second order language.  Which is yours? (If it turns out to be third order, a similar question arises.)  Once the language is fixed, there are such questions as do you have comprehension axioms?

https://en.wikipedia.org/wiki/Second-order_logic

First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations.

Second-order logic also includes quantification over sets, functions, and other variables as explained in the section Syntax and fragments.

Since my expression quantifies over set of relations (WFF) that would seem to make it 3rd Order Logic.

See next reply for more details:   Copyright 2017 Pete Olcott

The above analysis was made a little simplistic leaving out crucial details so that my explanation would not be overwhelming. Here are additional key details:

Here is the expression again taking it at face value it would be a third order logic expression:
∀x True(x) ↔ (∃Γ ⊆ SOL Provable(Γ, x)) ....

The actual language that I am using is Minimal Type Theory (and other formal languages with the same signature).

https://en.wikipedia.org/wiki/Signature_(logic)
In logic, especially mathematical logic, a signature lists and describes the non-logical symbols of a formal language.

https://en.wikipedia.org/wiki/First-order_logic#Non-logical_symbols
Non-logical symbols
The non-logical symbols represent predicates (relations), functions and constants on the domain of discourse. 

When Rupert asks what the signature of this language this is where things get more complicated.

This is the first time that I tried to address a question about the signature of a language. I addressed this question in terms of my current understanding of the signature of a function from computer science.

https://en.wikipedia.org/wiki/Type_signature
In computer science, a type signature or type annotation defines the inputs and outputs for a function, subroutine or method. A type signature includes the number of arguments, the types of arguments and the order of the arguments contained by a function.

So I am assuming that the signature of a language is the signature of its non logical objects.

[Pete Olcott]

The signature of the non-logical objects of MTT includes terms of arbitrary finite order as detailed below: 

Any WFF of MTT can be assigned an alias name and this alias name can be quantified thus providing the means for defining expressions of arbitrary finite order logic.

Syntax and semantics of the @ assign alias operator (how MTT assigns names to WFF)

LHS @ RHS assigns the LHS name to the RHS expression.

Example:
LiarParadox @ ~True(LiarParadox) // this expression refers directly to itself not indirectly to its name

Translated into a Directed Acyclic Graph (DAG) by the Minimal Type Theory (MTT) compiler
[01] LiarParadox (02)  // The name of the expression refers to the root node of its DAG
[02] NOT         (03)
[03] True        (01)  // cycle indicate infinite evaluation loop

The name of an MTT expression is an alias for the integer index of the root node of this expression's DAG just like a variable name in computer science is an alias for its memory address.

[Pete Olcott]

On 12/4/2017 1:39 AM, Rupert wrote:

On Monday, December 4, 2017 at 7:35:55 AM UTC+1, peteolcott wrote:

On Monday, December 4, 2017 at 12:16:39 AM UTC-6, Rupert wrote:

I clicked your first link. No definition of this language is given.

I have partial BNF on the first page of the second link. 

The actual BNF is totally complete, and I have a fully operational computer language compiler that translates these expression into directed acyclic graphs. I can't release the full BNF. 

The expressions that I am using now seem to be conventional second or third order logic. Thus their language is already defined. 

∀x True(x) ↔ (∃Γ ⊆ SOL Provable(Γ, x))

You're talking about a second or third order language? What signature?

I explained this in great depth in my three part reply to Percival.
I will sum it up here if you want additional details please see my three part reply to Percival. 

This is the first time the I have ever answered a question about the signature of a language thus I am answering this question to some degree in terms of my current understanding of the definition of the signature of a function from computer science.

The actual signature of the set of languages that I am defining is specified by the syntax of Minimal Type Theory.  MTT provides the means for any WFF to be assigned an alias name, and for any alias name to be quantified.  This provides the means for specifying expressions of arbitrary finite order logic.

It is very important to totally understand the precise syntax and semantics of MTT alias names because this key distinction is entirely different than the infinite hierarchy of indirect reference that Tarski referred to. 

[Pete Olcott]

On 12/4/2017 12:46 PM, Rupert wrote:

You misunderstood what is meant by the signature of a language. It just means the set of non-logical symbols. You have not, anywhere in this thread, given a definition of the language of MTT.

I have not redundantly provided this material directly in the thread, I provided much of it on the referenced links.

When someone asks me to define a language I do not cut-and-paste a whole dictionary. I provide a link to this dictionary.

The set of MTT non-logical symbols (as you would already know) is an infinite set. The syntax and semantics for defining this infinite set was provided on the referenced links and augmented with further explanation in this thread.

These links will be updated to include these augmented explanations:
http://liarparadox.org/Minimal_Type_Theory.pdf
http://liarparadox.org/Provability_with_Minimal_Type_Theory.pdf

[Pete Olcott]

On 12/5/2017 10:29 AM, Rupert wrote:
> On Tuesday, December 5, 2017 at 5:22:31 PM UTC+1, peteolcott wrote:
>> On Tuesday, December 5, 2017 at 10:05:43 AM UTC-6, Rupert wrote:
>>> On Tuesday, December 5, 2017 at 3:53:54 PM UTC+1, peteolcott wrote:
>>>> On Tuesday, December 5, 2017 at 4:16:51 AM UTC-6, Rupert wrote:

>>>>> Yes, I've read all that. There's no definition of what the language is. Do you understand what is involved in defining a language? First of all you need to define what the symbols are. What are the symbols?
>>>> This is what I count as a language definition, is this not what you count?
>>>> https://groups.google.com/d/msg/comp.compilers/Qalayu9h3xw/gaTrXbbRd7AJ
>>>>
>>>> %token PREDICATE FUNCTION CONSTANT VARIABLE
>>>> %token IMPLIES AND OR IFF THERE_EXISTS FORALL
>>>> %left '='
>>>> %left VARIABLE
>>>> %left IMPLIES
>>>> %left IFF
>>>> %left AND
>>>> %left OR
>>>> %left NOT
>>>> %%
>>>>
>>>> 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
>>>> ;
>>> I thought you said it was a second or third order language? Where are the second-order variables?
>> I am first getting mutual agreement on exactly what kind of language specification would be sufficient. The above is the complete language specification for first order predicate logic: FOPL.
>>
>> I stayed up until 1:00 AM working on redesigning my language specification for MTT such that MTT has absolute minimal divergence from the syntax of FOPL.
>>
>> MTT is an unlimited finite order of logic. The expression that I wrote only required 3rd order logic because it quantified over sets of relations. When implemented in MTT each one of these relations can be relations of relations of relations hundreds of levels deep.
> Well, that's all well and fine, but I don't understand that notation. Where can I read an explanation of how the notation works?
Percival is correct this is Backus Naur Form.
The references get quite involved for the simple explanation that is required.

*BNF is simply a recursive specification hierarchy.*

{sentence} at the top left is the root of the recursive specification tree.
All objects on the LHS are defined by the alternatives on their RHS.

The tree defines the syntax of any context free language. The list of tokens at the top of this specification define the words of this language, and thus the leaves of the parse tree.

For computer languages regular expression grammar defines the finite strings that comprise each individual token (word of the language).

[Pete Olcott]

On 12/5/2017 10:39 AM, Peter Percival wrote:
> peteolcott wrote:
>
>

>> I am first getting mutual agreement on exactly what kind of language specification would be sufficient. The above is the complete language specification for first order predicate logic: FOPL.
>

> Look in Mendelson (section 2.1 in the 5th ed.): you need to specify what the constants are, what the predicate letters are and what the number of places of each is, and what the function letters are and what the number of places of each is.
>
>
This will all be subsumed by defining an _IDENTIFIER with this regular expression:

D      [0-9]
L      [a-zA-Z_]
({L}|{UTF_8})+({L}|{D}|{UTF_8})*   { count(); return _IDENTIFIER; }

_IDENTIFIER ∈ Constants
_IDENTIFIER ∈ Predicates
_IDENTIFIER ∈ Functions

Specifying the arguments to Predicates and Functions will have its own separate syntax. Square_Root("egg sandwich") will be rejected as type mismatch error.

One of the huge changes to MTT will be that type specification may be optional in the same way that it is optional in FOPL, thus enabling MTT to evaluate FOPL expressions.

[Peter Percival]

Pete Olcott wrote:

> Specifying the arguments to Predicates and Functions will have its
> own separate syntax. Square_Root("egg sandwich") will be rejected as
> type mismatch error.

If, in first order logic, 'Square_Root' is a one-place function letter
and '"egg sandwich"' is an individual constant, then 'Square_Root("egg
sandwich")' is a constant term and it denotes an individual. If
'Square_Root' is a one-place predicate constant and '"egg sandwich"' is
an individual constant, then 'Square_Root("egg sandwich")' is a
sentence, though I suspect that you do not intend 'Square_Root' to be a
one-place predicate constant. 'Type mismatch error' is not something I
have come across in accounts of FOL: finite strings of symbols are
well-formed terms or formulae, or they are ill-formed. Function are
*total*.

I conclude that the syntax of MTT is *not* the syntax of FOL.

> One of the huge changes to MTT will be that type specification may
> be optional in the same way that it is optional in FOPL, thus
> enabling MTT to evaluate FOPL expressions.

'Type specification', optional or otherwise, is not something I
have come across in accounts of FOL.

Are clp or cap folk interested in any of this?


>


--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan

[Peter Percival]

Peter Percival wrote:


> [...] Function are

I meant 'Functions'.

> *total*.

See, if you wish,
http://www.ai4fm.org/events/ko-meeting/matthew-lovert-logic-partial-functions.pdf,
https://link.springer.com/chapter/10.1007/978-3-642-14203-1_18,
http://www.sciencedirect.com/science/article/pii/0304397590900053,
etc, etc.

> I conclude that the syntax of MTT is *not* the syntax of FOL.


>
>

[Pete Olcott]

On 12/5/2017 11:31 AM, Jim Burns wrote:

On 12/5/2017 10:42 AM, peteolcott wrote:

On Tuesday, December 5, 2017 at 8:53:54 AM UTC-6,

I count this as a complete language specification because
this is all that is needed to automatically generate a
computer program that can accept finite strings as
belonging to FOPL the language or reject finite strings
as not belonging to *the* FOPL language.

*emphasis added*

There is an essential point that you've missed:
It is not correct to say *the* FOPL language. There are
many. The first step in specifying a particular first-order
formal system is to say *which* FOPL language is being used.

https://en.wikipedia.org/wiki/First-order_logic
Using conventional terminology you would probably be correct, so what I am speaking of (when I talk about FOL) would be more accurately described at the set of languages having FOPL properties.

Likewise when I speak of languages that have no specific limitation regarding their logic order I am referring to a set of languages. 

Any language capable of expressing every aspect of every relation between (or among)  every element of the { set / collection / proper class } of all things I will call a Meta-Language (Improving, extending and correcting Tarski's version).  MTT is a Meta-Language

For example, the usual description of the set theory ZFC
has one undefined binary predicate in its language, 'e'.
   x e y == 'x is an element of y"

Meta-Languages (as their name implies) are capable of defining the semantics of their object language as Tarski has proposed.

As I have specified the term a Meta-Language is capable of defining the semantics of any other language, thus a proper superset of any non Meta-Language.

What is enormously more difficult to understand (Tarski could not quite understand this) is that a Meta-Language is also capable of defining its own semantics. 

MTT can and does contain its own complete and consistent truth predicate. This thread is devoted to this one aspect of MTT.

There are other things _defined_ in ZFC, set equality,
the empty set, functions, etc etc etc, and they will often
have notations _defined_ for them, but those are all defined
by (eventually) expressions using only 'e' and the usual
first-order suspects: variable names, logical operators,
quantifiers, parentheses, commas.

Equality is _defined_ in ZFC as
   x = y  :<->
      Az:( z e x  <->  z e y )
So, even though we see expressions in the language of
set theory with '=' in them all the time, the _answer_
to the question "What language is ZFC using?" does not
include "=". It's L('e'), just the one binary predicate,
like I said.

----
Your language description appears to need fixing.
I think I've mentioned this before, but it doesn't
seem to matter to you.

It is not that it needed fixing as much as the fact that I kept most of the details as is a trade secret.
I have published the BNF of some of the key enhancements that MTT adds to FOL.

I am in the process of redesigning MTT so that it will be able to evaluate FOPL expressions without modification to the syntax these expressions.  For example:  LiarParadox ↔ ~True(LiarParadox)  // Is this actually SOL ?

The above is actually only a paraphrase of the Liar Paradox this original MTT specification is exactly and precisely the actual Liar Paradox:
LiarParadox @ ~True(LiarParadox)

_As written_ , this parses as a sentence:
   VARIABLE = VARIABLE
It's probably not what you intend. It's certainly not
an FOPL sentence.

Here is a language definition for set theory:

name
   : 'x'
   | 'y'
   | 'z'
   | name \'
   ;

formula
   ; '(' name 'e' name ')'
   | '~' formula
   | '(' formula '->' formula ')'
   | 'A' name ':' formula
   ;

This is enough to define the rest of what we usually call
the language of set theory

   Ex:P  <def>  ~Ax:~P
   ( P \/ Q )  <def>  ( ~P -> Q )
   ( P /\ Q )  <def>  ~( ~P \/ ~Q )
   ( P <-> Q )  <def>  ((P -> Q) /\ (Q -> P))

   ( x sub y )  <def>  Az:(( z e x ) -> ( z e y ))
   ( x = y )  <def>  (( x sub y ) /\ ( y sub x ))

And so on.

If we give axioms and inference rules for that binary
predicate 'e', we will have _implicitly_ given axioms and
rules for all of these defined expressions, and much more.

It is in this "implicitly axiomatized" sense that we could
say we _understand_ something like the least upper bound
property of the set of real numbers, even though there
are many layers of definitions between L('e') and the
language which we would use to express the LUB property.
The expression of the LUB property can be _reduced to_ an
expression in L('e'), and we give rules and axioms for
manipulating expressions in L('e').

When Rupert asks you what your language is, he is asking you
for a list of symbols (the signature of the language) that
you will then give us the rules and axioms for using -- and
when you are done with that, you are done describing your
formal system. Anything you tell us after that will need to
be referred back to the language and rules and axioms you
have already told us. (Compare to how '=' gets referred
back to rules/axioms about the use of 'e'.)

Maybe it would be helpful for you to consider MTT a Meta-Language (a language for specifying languages) then maybe we could have a little deeper mutual understanding.

----
To sum up:

What you have there is NOT a description of the language of
MTT that you would be willing to draw a line under and say
"Everything after this point will be translatable to what
we have above this line."

  (I'm pretty sure about that, but if you think otherwise,
   go ahead and say so. You'll be asked to _use_ that
   definition, I hope you know.)

With this in mind for what I mean (and I'm pretty sure
Rupert means) by "definition of the language of MTT",
_what is your definition of the language of MTT_ ?

The BNF grammar that I published for FOPL was originally published on comp.compilers the moderator of this group is the author of the best selling book on lex and yacc (most popular BNF processing tools to automate the process making computer language compilers).

The best that I can tell this specification correctly recognizes every finite string that corresponds to this language description:
https://en.wikipedia.org/wiki/First-order_logic 

When my updated BNF grammar does the same for MTT expressions I will consider my language specification sufficiently complete.

To put this in technical terms as soon as I have a membership decider for MTT, then MTT is sufficiently defined.

[Pete Olcott]

On 12/5/2017 12:45 PM, Peter Percival wrote:

Pete Olcott wrote:

Specifying the arguments to Predicates and Functions will have its
own separate syntax. Square_Root("egg sandwich") will be rejected as
type mismatch error.

If, in first order logic, 'Square_Root' is a one-place function letter
and '"egg sandwich"' is an individual constant, then 'Square_Root("egg
sandwich")' is a constant term and it denotes an individual.  If
'Square_Root' is a one-place predicate constant and '"egg sandwich"' is
an individual constant, then 'Square_Root("egg sandwich")' is a
sentence, though I suspect that you do not intend 'Square_Root' to be a
one-place predicate constant.  'Type mismatch error' is not something I
have come across in accounts of FOL: finite strings of symbols are
well-formed terms or formulae, or they are ill-formed.  Function are
*total*.

I conclude that the syntax of MTT is *not* the syntax of FOL.

The language specification of Minimal Type Theory will be in the class of Meta-Languages that are capable of formally specifying every aspect of every relation between every element of the set of all things.

I am planning on updating the language specification of MTT so that it will be capable of evaluating FOPL expressions.

By FOPL expression I mean that a finite string is measured against the formal definition of the class of FOPL languages and accepted or rejected on this basis.

[Pete Olcott]

On 12/5/2017 12:45 PM, Peter Percival wrote:

Pete Olcott wrote:

Specifying the arguments to Predicates and Functions will have its
own separate syntax. Square_Root("egg sandwich") will be rejected as
type mismatch error.

If, in first order logic, 'Square_Root' is a one-place function letter
and '"egg sandwich"' is an individual constant, then 'Square_Root("egg
sandwich")' is a constant term and it denotes an individual.  If
'Square_Root' is a one-place predicate constant and '"egg sandwich"' is
an individual constant, then 'Square_Root("egg sandwich")' is a
sentence, though I suspect that you do not intend 'Square_Root' to be a
one-place predicate constant.  'Type mismatch error' is not something I
have come across in accounts of FOL: finite strings of symbols are
well-formed terms or formulae, or they are ill-formed.  Function are
*total*.

I conclude that the syntax of MTT is *not* the syntax of FOL.

One of the huge changes to MTT will be that type specification may
be optional in the same way that it is optional in FOPL, thus
enabling MTT to evaluate FOPL expressions.

'Type specification', optional or otherwise, is not something I
have come across in accounts of FOL.

Sure you have a function has a domain and a range.  In Math this is restricted to sets of numbers.
In the class of Meta-Languages (as previously defined) this is not restricted to numbers.

[Pete Olcott]

On 12/5/2017 12:45 PM, Peter Percival wrote:

Pete Olcott wrote:

Specifying the arguments to Predicates and Functions will have its
own separate syntax. Square_Root("egg sandwich") will be rejected as
type mismatch error.

If, in first order logic, 'Square_Root' is a one-place function letter
and '"egg sandwich"' is an individual constant, then 'Square_Root("egg
sandwich")' is a constant term and it denotes an individual.  If
'Square_Root' is a one-place predicate constant and '"egg sandwich"' is
an individual constant, then 'Square_Root("egg sandwich")' is a
sentence, though I suspect that you do not intend 'Square_Root' to be a
one-place predicate constant.  'Type mismatch error' is not something I
have come across in accounts of FOL: finite strings of symbols are
well-formed terms or formulae, or they are ill-formed.  Function are
*total*.

I conclude that the syntax of MTT is *not* the syntax of FOL.

One of the huge changes to MTT will be that type specification may
be optional in the same way that it is optional in FOPL, thus
enabling MTT to evaluate FOPL expressions.

'Type specification', optional or otherwise, is not something I
have come across in accounts of FOL.

See also Mendelson Axiomatic Set Theory.
(The closest preexisting basis for what I am saying next)
n  ∈ ℕ   // n is an instance of the type of natural number
m ∈ ℝ   // m is an instance of the type of real number
P ∈ Minimal_Type_Theory    // P is a WFF of Minimal Type Theory
Γ ⊆ Minimal_Type_Theory   // Γ is a set of WFF of Minimal Type Theory