3 ms·

There's so much that's wrong with this comment. You're either ignorant of formal logic, or deliberately trolling. If the former: being ignorant isn't a crime, b

• pron 10y ago
  > Let's keep things civilized, okay? Formal verification of large, very complex real-world systems is what I do all day every day. If you don't understand what it is that I'm saying (and that's my fault -- I'm probably not clear enough) you can just ask. I'm a practitioner, not a theoretician, so I may make mistakes, but I think that in this particular case you are too attached to the typed LC to consider other reasoning systems (which, BTW, happen to be far more prevalent in the verification community). > This doesn't even make sense. A program can be run. What does it mean to “run a proposition”? Let's step back and consider the theory and then get to the specifics. Consider the set of all TMs (perhaps TMs isn't the best name because it may imply a specific programming model, but that is not my intent; I'm using the term here interchangeably with an abstract state machine, or a program). 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? A proposition about a TM constitutes such a subset. Under certain conditions, you can incorporate all DTMs in the set corresponding to the proposition into a single NDTM, which can also be run. Hence, there is a direct correspondence between propositions about programs (e.g., the program returns its input sorted) and NDTMs. Hence, you can most certainly run a proposition about programs (though perhaps not all propositions). The temporal logic of actions (TLA) is a complete logic in the sense that for every NDTM (or a DTM as a special case) there exists a (non-unique) TLA expression, consisting of the simple logical connectives, the priming operator (an action) and possibly LTL operators (describing say, fairness, properties) that describes that particular TM. But, of course, a TLA expression can be less precise, and describe a whole set of TMs -- a proposition. Therefore in TLA, propositions and programs are the same object. Here's Lamport in the opening paragraph introducing TLA in the 1993 paper[1]: Correctness of [an] algorithm means that the program satisfies a desired property. We propose a simpler approach in which both the algorithm and the property are specified by formulas in a single logic. Correctness of the algorithm means that the formula specifying the algorithm implies the formula specifying the property, where implies is ordinary logical implication. FYI, that paper has 2458 citations and is far from obscure. This theory is much better known in the software verification community than type theory (certainly when you consider it within the greater framework of temporal logics, of which TLA is one), and has had a greater impact -- both academic and real-world -- on formal methods, at least so far. Specifying programs as propositions in temporal logics was a modern theoretical turning point in CS, and has yielded two or three Turing awards (Pnueli in '96, Clarke et al. in '07, and Lamport -- at least partly for this -- in '13). > Even if I charitably interpret that as “decide its truth value”, well, not all propositions are decidable! This is where things are a bit tricky. For a complete treatment see the preliminaries section in this '88 paper by Abadi and Lamport[2]. > A proposition has a truth value - a proof does not. Of course, but there's room for interpretation here (like I said, I'm not a type expert so I'm not 100% sure about it): `<x = 3, y = 5>` can be viewed as a proof object of the proposition `∃x,y ∈ 1..10 . x < y`, but it can also be viewed as the more precise proposition, `x = 3 ∧ y = 5`. Existential propositions (or types) can therefore be viewed as a set of multiple programs, while the proof object is a particular program, that could have been specified with a more precise proposition. That is what I meant when I said "hidden proposition". If you step back from typed LC and consider the original proof objects, those objects are just a series (a tree, actually) of logical deductions. Each of those deductions is a proposition. A proof is, therefore, a series of true propositions, each derived from the previous one using one of the deduction rules. You can certainly say, then, that a proof is a collection of hidden (true) propositions. [1]: http://research.microsoft.com/pubs/64074/lamport-actions.pdf http://research.microsoft.com/pubs/64074/lamport-actions.pdf [2]: http://research.microsoft.com/pubs/64046/abadi-existence.pdf http://research.microsoft.com/pubs/64046/abadi-existence.pdf
  • catnaroek 10y ago
    > 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...