113 reputation
6
bio website
location Argentina
age 23
visits member for 2 years, 1 month
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.


Sep
17
comment What does the concept of computation actually mean?
It's not that I can't distinguish the concepts, my issue is accepting the fact that they cannot be "blended" together in any satisfactory way. For example, check the "Proof Explorer" presentation of the axioms of FOL as done by Norman Megill's Metamath site; the only two rules he introduces (MP and Gen) use symbols not included in the formalism presented. The whole idea of "having a closed description of a formalism" seems to fail as you always need an external input to perform the computation, i.e. the execution concept isn't self-contained.
Aug
30
comment What does the concept of computation actually mean?
I assert that in the case of having access to a TM which achieves universality, dealing only with formal descriptions of TM's is justified, because you can always feed the description to your UTM as a string of bits. Then you are free to blend together the notion of "object" and "description" because the computational behavior of the TM descripted, and the computational behavior of the UTM fed with the description of the TM, are indistinguishable.
Aug
30
comment What does the concept of computation actually mean?
I'd really appreciate if you could elaborate some more on the assertion that a TM is "computation embodied" in your answer, as it could answer my question indeed. I don't see the fundamental difference between "the description" and "the object" (without diving into the sea of the philosophical ontology of being, which I consider obfuscatory and ussually nonsense) because a TM is generally formalized as a tuple and so it is an abstraction, something we can only deal with by a formal description, and in the case of an UTM it seems justified.
Aug
30
comment What does the concept of computation actually mean?
@PeterSmith: what I try to point out is that your remarks are not evident, i.e. they don't simplify the issue by reference to simple and clearly recognizable concepts. If both sets of axioms ("propositional") and rules ("procedural") can be coded in a string of symbols and fed to a (physical) UTM -like any general purpose computer available today- which treats them equally as input (something "given" in the sense I used in my question), then the distinction you make isn't enough to make the question trivial and "massage away the temptation to ask it". Something else is going on here.
Aug
30
comment What does the concept of computation actually mean?
I don't see why you assume the difference you state between "propositional knowledge" and "procedural knowledge" to be a clear concept. Eighty years ago it could have been a reasonable argument to say so, but with today's ubiquitous computer devices it clearly isn't. Any computer program is an example of "procedural knowledge" in your sense, and every copy of it is coded up as a bit sequence and is indistinguishably treated by the CPU just like any data set (some "propositional knowledge"). So, even though you correctly recongnized the rationale behind the question, you didn't answer it.
Aug
30
comment What does the concept of computation actually mean?
But even if you abstract away the notion of an UTM to a bit-string describing the computational process (i.e. a piece of software written in an universal programming language), then you fall into the problem I was originally asking about -the UTM needs another UTM, an interpreter, to compute. Otherwise you seem to be stuck with the static bit-string, and a bit-string doesn't compute by itself; in essence, I could rephrase my question as "there's a way for a computational system to be closed on itself?", and its answer seems to be that it can't.
Aug
30
comment What does the concept of computation actually mean?
I understand that universality guarantees that any two UTM's can simulate each other (i.e. given one machine of the pair, and the piece of code which describes the transition functions of the other one, the computations performed on arbitrary input would be indistinguishable from the computations corresponding to the actual running of the UTM being simulated, and viceversa). That's why I don't feel the necessity to state that "a TM desription is not the same as the TM itself", at least when the TM is T-complete (i.e. an UTM).
Aug
29
comment What does the concept of computation actually mean?
@MarcvanLeeuwen: I'd appreciate if you could elaborate more on the fundamental difference between hypothesis and rules of inference, which makes it wrong to "place them on the same level". I tend to view everything needed for a computation to be performed, as pieces of code -and the encoding in a bit-string applies equally to premises and rules, with the obvious differences in syntax, and nothing else- because that's how a computer program is written down to machine code; but then I get troubled with the concept of "change" associated to the computational process itself, from input to output.
Aug
29
comment What does the concept of computation actually mean?
Addon: I always felt uncomfortable when reading the description of a rule of inference, like MP, and finding that it always seemed to require the inclusion of symbols not included in the formalism to express it (like: "Hyp_1" & "Hyp_2" $\Rightarrow$ "Assertion", or equally, the "horizontal bar" which separates premises of the conclusion in natural deduction systems). Is this feature a consequence of the fact that the computation (following the rule description, i.e. it's code) is always performed by an instance of some computer model "outside" the formal system you're describing?
Aug
29
comment What does the concept of computation actually mean?
So, does that mean that what I call the "dynamical" component of computation (i.e. what makes it a process, rather than a set of ordered pairs of input and output elements) is a concept always placed at a meta-level from the point of view of the description of the computation (i.e. what I call the "static" component -the bit string which encodes the input and the deductive rules, such as the three first items I listed above)? Given that universality implies that any T-complete computer program can simulate any other program, might then the role of the TM be to lie at the metalevel?
Aug
29
comment What does the concept of computation actually mean?
Both the "counting" and the "action" are computational processes -there's a formal description to do both, for example in PA. The issue is in the relation between the "description" of the computation and the computation itself (the quotation marks emphasize the fact that I'm not sure the description captures the concept, or most probably I'm missing something).
Jul
30
comment How are the full semantics of SOL and HOL specified?
I'd really appreciate if you could leave an answer there, because I didn't find any of the current ones satisfactory.
Jul
30
comment How are the full semantics of SOL and HOL specified?
Thank you very much. This question was related to another which I cite in the first paragraph; the sense of the word "fundamental" I used there, is more or less the same we've discussed here under the adjective "formal", except for the added meaning of being able to "simulate" other logics from a mathematical point of view (e.g. fuzzy logics can be formalized in a FO mathematical theory which supports the real numbers, and define the "fuzzy membership" as an ordered pair).
Jul
30
comment How are the full semantics of SOL and HOL specified?
I think you caught what I'm asking. In essence, the whole concept of "full semantics" is what troubles me. How can it be taken as a "well-defined" term, if higher order logics which fulfill categoricity need a FO meta-theory of set-theoretical flavour to prove the categoricity of what "they say" with their "more expressive power"? Where does the "expressivity" come from, if you've used a non-categorical set theory to prove it? If I get it right, it seems to be nearly the same problem as when considering the "standard universe" of set theory. It's just intuition? What's "formal" about that?
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.