[ontoiop-forum] DOL finalisation

[John F Sowa]

On 12/21/2017 7:25 PM, Pat Hayes wrote:
> If one restricts CL (Lw1-w) so that sequence markers (infinite
> conjunctions) occur only on the LHS of sequents, it is first order.
> ...  The mapping is pretty obvious once it is pointed out. > > (forall (…x)(FOO …x))> > maps to (and has exactly the same semantic 
truth conditions as)> > (and> 	(forall (x)(FOO x))> 	(forall (x1 x2)(FOO 
x1 x2))> 	(forall (x1 x2 x3)(FOO x1 x2 x3))> …)
As Pat's example shows, this restricted use of sequence markers
is a convenient notation for specifying axiom schemata.

FOL with axiom schemata is commonly used to specify set theory and/or
any mathematical structures definable in terms of set theory.

John