Re: what follows from denying an axiom

On Sun, 01 Feb 2009 01:02:20 -0700, Nam Nguyen <namducnguyen@xxxxxxx> said:
Chris Menzel wrote:
On Sat, 24 Jan 2009 13:57:07 -0700, Nam Nguyen <namducnguyen@xxxxxxx>
said:
george wrote:
...
Chris Menzel is the first person I have ever heard say "second-order
language".
Would he then be the one who wrote the content of

http://plato.stanford.edu/entries/logic-higher-order/

I wish!

I'd like to thank you and George for clarifications on this link.

I did write this one, however:

<shameless plug>

http://plato.stanford.edu/entries/actualism

</shameless plug>

Thanks also for this . [For what it's worth, I've been pursuing
what I'd call as "mFOL" (meta FOL) and these 2 links provide some
useful information, though I'm still "dwelling" on both of them,
being slow!].

Glad you found them helpful.

As in your response to Daryl, I think it's _syntactically_ possible to
tell if the reasoning is in fol or sol.

Reasoning was never an issue in my response to Daryl. My claim was only
that it is possible rigorously to define the notion of a second-order
language purely syntactically.

As for different "semantics" of "quantifying over..." individuals of
different sorts in SOL, I think we've opened a can of worm here.

As implied by Hilbert (or even Shoenfield), _formal_ system is sheer
syntactical and is *self-sustained* in the sense that reasoning with
it can be carried out *only with its axioms and the inference rules*:
one doesn't even have to know of any model at all, to infer a theorem.

That is of course quite correct.

Then syntactical reasoning is in effect just a mind game (i.e. in the
meta level) of syntax/symbol manipulation; just like when we take a
syntax-pattern-recognition test, from say the NSA. So, to paraphrase
what Boromir says of Gondor ("The Lord of the Rings"), we could safely
state:

Formal system has no semantics. Formal needs no semantics.
(Or no interpretation for that matter).

Whether or not the formal system is of 1st or 2nd order!

Again, that is quite true. The difference between the two, of course,
is that no purported system of second-order logic can be semantically
complete; for any such system, there will be second-order validities (in
standard second-order semantics) that are not theorems of the system.

Not only we could choose between Standard and Henkin semantics for
quantification of "individuals" of different sorts in SOL, we could
also come up with different semantics for the FOL symbols 'A' and 'E':
semantics that *has nothing to do with quantification* at all!

Well, yeah, sure, we can assign any semantics we want to the symbols of
a language.

All of which means semantics or interpretation is subjective

Now that doesn't follow *at all*. If I announce that I am assuming
Henkin's semantics to interpret a second-order language, my semantics is
from that point forward entirely objective in the given context. What
*is* the case is that a semantics doesn't "attach" to a given language
by magic; some such announcement is required. But once it is made in a
given context, the semantics is, within that context, as objective as
can be.

and hence is a weaker notion than that of syntactical provability.
Weaker in the sense that if a formula is a syntactical theorem, it's
always a theorem, while if a formula is true under some semantics or
interpretation, it could still be false under others.

I'm not sure I see the contrast. One has to define a proof theory for a
language L no less than one has to define a semantics. The same sentence
of L might be provable in one system and not provable in another.
Provability is thus relative to a proof theory, just as validity is
relative to a semantics.

I'd let go SOL (or any higher order) reasoning all together. And in
its place we could introduce mFOL (meta FOL). The idea of mFOL is that
in the meta level, an n-ary non-logical symbol could in fact be a
variable that might range over more than one constant-symbols. And in
the context of mFOL we could introduce:

(1) The concept of "global" theorems or provability.
(2) The concept of unknown-ability to mathematical reasoning,
making our reasoning a bit more humble than it has been
(since GIT).

Imho, both of these concepts would reflect more of a reality of difficulties
in mathematics that we've been facing. FOL, SOL and the like only mask the
reality.

I don't see the problems with FOL and SOL that you seem to, but perhaps
your approach could prove fruitful as well. You might google "metalevel
reasoning" for some work in AI that you might find relevant.


.

Relevant Pages

  • Re: what follows from denying an axiom
    ... to do with SECOND-order ANYthing, ... is just to make things more tractable BY DESCENDING TO FIRST-order. ... second-order language as a many-sorted first-order language. ... That is, for a sentence σ to be valid in the general semantics, it must ...
    (sci.logic)
  • Re: what follows from denying an axiom
    ... Chris Menzel is the first person I have ever heard say "second-order ... language purely syntactically. ... Formal system has no semantics. ... to the resultant perception-phenomenon known as relativity, ...
    (sci.logic)
  • Re: what follows from denying an axiom
    ... have almost exactly *my* characterization of Henkin's semantics! ... "second-order language" can be defined completely syntactically. ... meaning than the use of a first-order language, ...
    (sci.logic)
  • Re: Second-order and Higher-order Logic
    ... admits that it is basically talking about the Henkin semantics. ... by first translating second-order language into a typed first-order language. ... So there are two distinct logics here: ...
    (sci.logic)
  • Re: object system...
    ... conflict with the actual sun and stars (so, ... Interface too can have some properties defined in terms of third types ... not the language or its target. ... If you ignore overflow exceptions, then necessary, the semantics becomes ...
    (comp.object)