113 reputation
7
bio website
location Argentina
age 23
visits member for 2 years, 3 months
seen Mar 15 '13 at 16:31

I'm just a engineering student, but also a dabbler to deeper topics, at least deeper than those proposed by my academic choice.

That's why I'm here.


Jul
30
awarded  Supporter
Jul
30
comment How are the full semantics of SOL and HOL specified?
Then, I can't see why the sentence "SOL can define the reals to be the only complete Archimedean field up to isomoprhism" can be formally taken as meaningful. If we write down a SO theory, and then add a FO deductive system augmented with comprehension and choice axioms, it turns out that it loses expressive power (and becomes equivalent to FOL by Lindström's theorem); but if we don't include those axioms, then "it's categorical" and "more expressive", but only when provided a model from a meta-level and not "by itself".
Jul
30
comment How are the full semantics of SOL and HOL specified?
@CarlMummert: the whole problem is that I'm talking about the formalization of the semantics of a logic within it, just because it seems to me that's the only meaningful way of asserting categoricity (if it's possible). In FOL that doesn't involve a meta-level, because it's completeness guarantees the matching between provability and satisfaction by (at least) one model. But in higher order logics the failure of completeness means that their semantics must be considered necessarily from a meta-level; and so, as you say, the elimination of possible models must be carried out at that level.
Jul
30
comment How are the full semantics of SOL and HOL specified?
@HenningMakholm: I brought the issue of categoricity and models just because that is what I wanted to ask originally (about full semantics of logics higher than FOL). If HOL syntax is always "translatable" to a FO set theory syntax -be it single-sorted like ZFC or many-sorted, like the two-sorted axiomatization of NBG-, and then the only thing which HOL does is making formalization of deduction systems less cumbersome (at the only cost of "moving the line" of what can be philosophically argued to be the limit between logic and mathematics), then you should add this to your answer.
Jul
30
comment How are the full semantics of SOL and HOL specified?
Furthermore: isn't then absolute categoricity (i.e. the claimed result for theories such as the SO formalization of the reals under it's full semantics) not a meaningful property for theories based on any logical order, if we need (for example) an additional FO set theoretical, non-categorical meta-language to produce a model for it, which just then can be proved to be unique in reference to it's axioms? Or what amounts to the same conclusion: isn't then only relative categoricity a meaningful property of a formal theory under, any logic?
Jul
30
comment How are the full semantics of SOL and HOL specified?
Well, I suppose that the kind of logical axioms you refer to are, for example, the comprehension and choice axioms in SOL. If I undestood what you said, then both SOL and HOL can be effectively matched with a suitable MS-FOL; so, might it be argued that the only difference between these rests on the way "higher order" variables are formalized (in the former by comprehension, and in the latter by the proper signature of the many-sorted model, i.e. the sorting of the arities of functions and relations)? It's just that FO formalization is cumbersome, and there's nothing else?
Jul
29
comment How are the full semantics of SOL and HOL specified?
What confuses me is that, even if your argument is absoltely sound (computers only follow syntactical rules and don't care about semantics), then it seems to follow that every logic of a higher order than FOL is necessarily computed like if it was a many-sorted FOL (i.e. doesn't recognizing, for example, that second-order variables range over subsets of the same set which first-order variables range over). I suspect I'm missing something here, though.
Jul
29
asked How are the full semantics of SOL and HOL specified?
Jul
28
revised Is First Order Logic (FOL) the only fundamental logic?
added 479 characters in body
Jul
28
awarded  Editor
Jul
28
revised Is First Order Logic (FOL) the only fundamental logic?
deleted 3 characters in body
Jul
28
awarded  Student
Jul
28
asked Is First Order Logic (FOL) the only fundamental logic?