4 ms·

> Consider the set of all TMs (...) Each and every one of them is "runnable", right? Each and every subset of that set also consists of TMs, which are also runn

> Consider the set of all TMs (...) Each and every one of them is "runnable", right? Each and every subset of that set also consists of TMs, which are also runnable, right? This much makes sense. > A proposition about a TM constitutes such a subset. A unary predicate whose argument ranges over TM may have such a subset as its extension. Two syntactically different predicates may have the same extension. > If you step back from typed LC At this point I'm not even talking about types. I'm talking about deductive systems in general. > and consider the original proof objects, those objects are just a series (a tree, actually) of logical deductions. This part is correct. > Each of those deductions is a proposition. Propositions exist inside of a logic, deductions exist in the logic's metatheory. There oughtn't even be the possibility of conflating them. > A proof is, therefore, a series of true propositions, each derived from the previous one using one of the deduction rules. A deduction is a series of judgments related by rules of inference. But a judgment is not a proposition!

pron 10y ago
> A unary predicate whose argument ranges over TM may have such a subset as its extension. Yes, but now we can talk about a specific logic/language, and now it matters exactly how the NDTM is expressed syntactically. E.g. in TLA (and LTL, or CTL for that matter) `[](x ∈ {1,2,3})` means "the variable x in the program is always in 1..3", or (semantically) "the set of all TMs where x is always in 1..3". x is a name given to a variable in an infinite set of variables defining the abstract machine's state (i.e. a state in TLA is defined to be an assignment to the infinite set to all possible variables), and the existence of the machine (or a Kripke structure, if you will) is implied. If you only supply a proposition on variable x, it means that all other (infinite set of) variables can take any value. You can read about TLA/TLA+ in one of the links I provided to get the specifics (it's extremely easy to pick up, BTW). In any event, a proposition in TLA can be thought of as a predicate over a(n implicit) TM. You may also find this short note by Lamport about the history of TLA/+ (and in particular the unification of temporal-logic propositions and programs) interesting[1]. > Two syntactically different predicates may have the same extension. True, I didn't say the syntactic representation is unique. Also, in TLA it's no longer just a predicate but any proposition. > There oughtn't even be the possibility of conflating them. I am not conflating them, and I'm not saying a proof is formally a proposition. I'm saying that in intuitionistic logic, a proof (especially of an existential quantification) may be also interpreted as a more precise/limited proposition. But this is just a vague notion, and it could be completely wrong (even if I were able to communicate it clearly), so I see no point in debating this. [1]: http://research.microsoft.com/en-us/um/people/lamport/pubs/commentary-web.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/c...

pron 10y ago

> A unary predicate whose argument ranges over TM may have such a subset as its extension. Yes, but now we can talk about a specific logic/language, and now it matters exactly how the NDTM is expressed syntactically. E.g. in TLA (and LTL, or CTL for that matter) `[](x ∈ {1,2,3})` means "the variable x in the program is always in 1..3", or (semantically) "the set of all TMs where x is always in 1..3". x is a name given to a variable in an infinite set of variables defining the abstract machine's state (i.e. a state in TLA is defined to be an assignment to the infinite set to all possible variables), and the existence of the machine (or a Kripke structure, if you will) is implied. If you only supply a proposition on variable x, it means that all other (infinite set of) variables can take any value. You can read about TLA/TLA+ in one of the links I provided to get the specifics (it's extremely easy to pick up, BTW). In any event, a proposition in TLA can be thought of as a predicate over a(n implicit) TM. You may also find this short note by Lamport about the history of TLA/+ (and in particular the unification of temporal-logic propositions and programs) interesting[1]. > Two syntactically different predicates may have the same extension. True, I didn't say the syntactic representation is unique. Also, in TLA it's no longer just a predicate but any proposition. > There oughtn't even be the possibility of conflating them. I am not conflating them, and I'm not saying a proof is formally a proposition. I'm saying that in intuitionistic logic, a proof (especially of an existential quantification) may be also interpreted as a more precise/limited proposition. But this is just a vague notion, and it could be completely wrong (even if I were able to communicate it clearly), so I see no point in debating this. [1]: http://research.microsoft.com/en-us/um/people/lamport/pubs/commentary-web.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/c...