From: Nam Nguyen on
Aatu Koskensilta wrote:
> Nam Nguyen <namducnguyen(a)shaw.ca> writes:
>
>> Another example would be suppose we define AI formal system as one in
>> which some of its theorems would be syntactically isomorphic to a
>> formal system in which in turn there's a formula than can't be model
>> theoretically truth definable. The clause "a formula than can't be
>> model theoretically truth definable" would require a close inspection
>> of our current knowledge about the foundation of reasoning via FOL.
>
> Well, the notion of a formula being "syntactically isomorphic to a
> formal system" also needs some elucidation.
>

I'll make an explanation on this as soon as I could. But what did you
mean by "also"? What else did you have in mind that would need
clarification?
From: Nam Nguyen on
Aatu Koskensilta wrote:
> Nam Nguyen <namducnguyen(a)shaw.ca> writes:
>
>> I'll make an explanation on this as soon as I could. But what did you
>> mean by "also"? What else did you have in mind that would need
>> clarification?
>
> The notion of "a formula that can't be model theoretically truth
> definable", which you yourself said "would require a close inspection of
> our current knowledge about the foundation of reasoning via FOL".
>


I see. OK first your first request of clarification:

Aatu had:

> Well, the notion of a formula being "syntactically isomorphic to a
> formal system" also needs some elucidation.

Say, Q is finitely axiomatizable in the language L(0,S,+,*,<) with n-axioms
A1, A2, ..., An. Now let form an overall formula:

A = A1 /\ A2 /\ ... /\ An

Now let L' = L'(0',S',+',*',<')

and let A' be A but with any non-logical symbols in L be syntactically
replaced by the counterparts in L'. Then A' would be "syntactically isomorphic
to a formal system": at least to Q.

***

Now back to your other request for clarification. Suppose we only have
a partially constructed model with, say a partially predicate set, then
there could exist a formula "that can't be model theoretically truth
definable" [or "evaluated-able"]. For example, if U = {1, 2, 3, ...}
where all it's elements are supposed to be ZF (model) sets, then
here we'd would have an incompletely specified U, and so the formula:

F <-> Ex1x2x3x4x5x6x7x8x9x10[ "All x's are pairwise distinct" ]

would not be model theoretically truth evaluated-able, assignable,
definable, or any similar words.