Doug Spoonwood
Reputation
5,579
Top tag
Next privilege 10,000 Rep.
Access moderator tools
 12h answered $(A_1\rightarrow\wedge A_2)$ is not a well-formed formula 12h comment $(A_1\rightarrow\wedge A_2)$ is not a well-formed formula @CarlMummert I don't know how to prove that binary operators are never adjacent. I do think I could fairly easy prove that the sum of the number of sentence variables and constants has to equal one more than the number of binary connectives (given that no connectives with arity greater than 2 exist in the formula). The property that binary operators are never adjacent is local to infix schemes. The property that (#(connectives) + 1) = #(sentence variable and constants) holds for prefix, infix, and postfix schemes. 13h comment $(A_1\rightarrow\wedge A_2)$ is not a well-formed formula "∧ only can appear between sentence symbols: A∧B." Huh? $\land$ appears between parentheses and sentence symbols. E. G. (A $\land$ (B $\lor$ C)) or (A) $\land$ (B) in another infix scheme. That said, if you ignore improper symbols, then maybe $\land$ can only appear between sentence symbols. 1d comment mathematical proof vs. first-order logic deductions @MichaelHardy So, given that computers can never understand anything, the possibility of a computer ever proving something is impossible in principle? EQP didn't prove anything at all, it just indicated symbols to get printed to the screen? I certainly don't agree that understanding proves something. Understanding is psychological. Proofs on the other hand are objective, and thus I think you've made a category error. 1d comment mathematical proof vs. first-order logic deductions The four square theorem implies that in any legitimate, prefix, infix, or postfix notation certain patterns hold (given the same variables and operations symbols used). But, say a meta-theoretic proof using the Deduction Theorem only implies that in this particular formal language, we have that say from {$\gamma$, p} $\vdash$ q we can move to $\gamma$ $\vdash$ Cpq. It doesn't imply a similar result in an infix scheme. That said, there does exist a meta-theorem which implies that such a result will exist in another notational scheme, but the proof of the Deduction Theorem doesn't do that. 1d comment mathematical proof vs. first-order logic deductions The meta-theoretic proofs thus aren't of the same type of proof-style as classical mathematics, in that they establish results about well-defined symbolic objects. A classical mathematics proof, on the other hand, given such as correct, establishes a result about certain ideas. That every number equals the sum of some four square numbers does have implications for symbolic objects, but ultimately comes as conceptual, since numbers are not symbolic object, but rather qualify as conceptual. A meta-theoretic proof is more particular than that... 1d comment mathematical proof vs. first-order logic deductions The style of meta-theoretic proofs isn't quite the same as in classical mathematics, because in classical mathematics we don't necessarily have well-defined statements to begin with. For instance, we might prove some number-theoretic result that says that under certain conditions for a, b, and c, a + b = c. The grammar involved in such an equality though is not well-defined. From a formal point of view, the grammar for something like a + b = c is defined before any proof takes place, which basically means that '=' is a binary predicate, '+' is a binary operation, and a unique parsing order. 1d comment mathematical proof vs. first-order logic deductions " You say it is difficult to formalize meta-theoretic proofs, aren't then these proofs in a way more basic then the ones written in first-order logic?" No. Meta-theoretic proofs tell us something about the system. The results they give (at least from what I have seen of them) can get obtained without those results. For instance, say you have some demonstration using the implication of The Deduction Theorem that you can discharge a hypothesis and a conclusion into a conditional. This ultimately implies that a formal proof exists without The Deduction Theorem. 1d comment mathematical proof vs. first-order logic deductions "You write proofs to convince yourself..." No, I don't always write proofs to convince myself of something. Even in say number theory, one might try to prove some theorem which we already know to hold as true, just in a different way. Some constructivist mathematicians might do this regularly, because they may well feel convinced by non-constructive proofs and most mathematicians stand convinced by those proofs also. Also, if proof is a construct created by the society of mathematicians, then how do certain programs generate proofs? Are the programs mathematicians? 1d comment mathematical proof vs. first-order logic deductions "Likewise proofs studied in mathematical logic, written in a form suitable to submit them to proof-checking software, are not proofs" So would you maintain that EQP (and other theorem provers that have produced new results), didn't prove anything at all when it returned a proof of the Robbins Conjecture for William McCune? 1d comment mathematical proof vs. first-order logic deductions Michael Hardy's comment "Likewise proofs studied in mathematical logic, written in a form suitable to submit them to proof-checking software, are not proofs" makes no sense at all and probably could accurately get said to consist of little more than posturing. A logician could similarly posture and say that no proofs in mathematics exist, and that proof is a logical concept, and thus only proofs exist inside the context of logic. Also, the comment makes no sense in light of the fact of computer generated proofs which have produced new mathematical results. 1d comment mathematical proof vs. first-order logic deductions Also, I don't write proofs just to convince myself of the truth of some theorem, or that it appears in some system. One problem consists of finding the shortest proof or a shorter proof under some fixed axioms and rule(s) of inference. In those cases, I'm almost always already convinced that the theorem exists in the system, and I'm not trying to convince myself again that such holds! I'm trying to find a shorter proof. Or maybe I'll try to find a proof that uses fewer variables, fewer axioms, or comes as more easily followed, say by only requiring a unification to occur in one way. 1d comment mathematical proof vs. first-order logic deductions 1. Go ahead and try to formalize meta-theoretic proofs if you want to. I believe that many experts would consider that a difficult exercise. You'll need a different meta-theory to avoid circularity. 2. I whole heartedly disagree with Ethan Bolker's comment that proof is a social construct, and I believe that the people like Russell, Frege, Lukasiewcz, etc. who founded mathematical logic would resolutely stand against such an instance of social psychologism. I also have the opinion that, strictly speaking, proofs qualify as logical entities, not mathematical entities. 1d answered mathematical proof vs. first-order logic deductions 1d comment Normal Submagma? What does x.H stand for? Is "." an operation? 2d comment How to prove that a statement is a theorem using Hilbert's system? Interesting approach. Did you prove each of the rules that you used here first using just substitution and detachment? Also, (¬C→(B→(A→B))) is a special case of a more general theorem. 2d comment How is prolog's expressiveness more restricted than First Order Logic? Can you have rules like the first-order rules of demodulation and paramodulation in Prolog? This source might have some relevance: ai.sri.com/~stickel/pttp.html Jul3 comment Intuitionistic Proof of $(a \Rightarrow b) \Rightarrow (\lnot b \Rightarrow \lnot a)$ You don't necessarily need to recall that Nx is an abbreviation for Cx0 necessarily, though that will suffice. You could have CCp0Np as an axiom, which isn't quite the definition. Jun29 answered Solve it by using logical proposition Jun27 comment How Do You Show That There Exist Infinitely Many Organic Tautologies? Oh and extended forms of importation and exportation like you've suggested with your last comment should work also.