Doug Spoonwood
Reputation
6,141
Top tag
Next privilege 10,000 Rep.
Access moderator tools
 Apr 23 answered Prove the following using only axioms of propositional logic and the deduction theorem? [see description] Apr 20 comment Can some mathematical objects exist without set theory? "This system proves theorems in "the classical equivalential calculus" — a first order theory of equivalence?" It's actually a zeroth order theory. The classical equivalential calculus has all tautologies which only have a symbol for logical equivalence in them. I'm not so sure that Prover9 or OTTER qualify as a realization of constructive set theory, since they work mainly via first order resolution. Apr 20 comment Can some mathematical objects exist without set theory? @BrianO Here's a link to a paper with a short description of an automated theorem prover: projecteuclid.org/download/pdf_1/euclid.ndjfl/1093888213 How is that a realization of constructive set theory? Apr 19 comment Can some mathematical objects exist without set theory? " If you're a formalist, then no, the objects of consideration have no independent existence, and, visualize what we may, only the formal systems, marks on paper and screens, really exist. " If so, then how can results from automated theorem programs fail? The formal systems don't necessarily require set theory. And some don't even have set theory. Consequently, mathematical objects don't hinge on sets for a formalist. "There's no theorem that answers these questions, and there's no "right" answer; it's more a matter of disposition and belief." Apr 19 comment Formal logic proof verification Step 8 is not correct. Apr 19 answered Can some mathematical objects exist without set theory? Apr 19 comment Can some mathematical objects exist without set theory? Do fuzzy subsets end up under the scope of set theory? Or rough sets? Apr 18 answered Showing that $(A \land B)' \land (C' \land A)' \land (C \land B')' \to A'$ without a truth table Apr 18 comment A faster way of proving that a 'theorem' (logic) is true. The logical law that underpins this is CCNpKqNqp. Apr 18 comment A faster way of proving that a 'theorem' (logic) is true. The logical law that underpins this is CCNpKqNqp. Apr 16 comment In what formal proof systems is the deduction theorem taken as a primitive rule of inference? In something like CpCCpqq, we can extend propositonal calculus by writing something like $\forall$p$\forall$q CpCCpqq. And thus we can use universal quantifiers over an entire formula. But, we can't do this in something like p, Cpq $\vdash$ q. Use of the rule of conditional introduction can pass from p, Cpq $\vdash$ q to CpCCpqq, but the use of that rule completely misses the distinction between the variables between those two things. There also Hilbert-Frege systems with functorial variables, but if conditional introduction gets taken on a priori, that sort of extension isn't so happy. Apr 16 comment In what formal proof systems is the deduction theorem taken as a primitive rule of inference? @HansBrende There's a little more to it. In Hilbert-Frege systems we have a rule of uniform substitution (or we can use substitution instances of any axiom or theorem). If you have conditional introduction as primitive rule of inference in a Hilbert-Frege context, you need to re-formulate that rule, because you can't use the rule of uniform substitution on any formula in a derivation which starts with a hypothesis which gets discharged. From another perspective, the variables in something like p, Cpq, $\vdash$ q, differ from those in CpCCpqq. Apr 15 comment In what formal proof systems is the deduction theorem taken as a primitive rule of inference? And having dependent axioms or rules of inference violates the principle of parsimony, or "Occam's Razor". As long as simpler theories should get preferred in their foundations, that implies that what Wikipedia suggests to do shouldn't get done. Apr 15 comment In what formal proof systems is the deduction theorem taken as a primitive rule of inference? Additionally, even if the terminology here was not so poor, if say the rule of conditional introduction got taken as a primitive rule of inference in a Hilbert System with modus ponens and appropriate axioms such as (in Polish notation), CpCqp, CCpCqrCCpqCpr, then the rule of conditional introduction becomes derivable in that system. Addiitonally, CpCqp, and CCpCqrCCpqCpr stand as derivable from just the rule of conditional introduction and modus ponens (which is needed to prove the deduction theorem). Thus, independence of rules and axioms doesn't hold. Apr 15 comment In what formal proof systems is the deduction theorem taken as a primitive rule of inference? This part of wikipedia got wrote poorly. In natural deduction systems, you don't have a rule of inference called the deduction theorem. You have a rule of inference which says "from $\gamma$ U {A} $\vdash$ B, you may infer $\gamma$ $\vdash$ (A -> B)," which can get called conditional introduction. The deduction (meta) theorem consists of an if ... then statement about propositions. Thus, you have to use modus ponens to apply the deduction theorem and modus ponens. Apr 2 comment Truth table and induction If $\bot$ is a wff, then you only need →. Mar 10 answered Looking for in depth material on a formal propositional calculus using only the NAND connective Feb 15 comment Examples of properties not preserved under homomorphism @MusaAl-hassy Homorphisms don't preserve commutavity for the entire structure. Jan 21 comment Proof in Propositional Logic of Peirce's Law I don't see how you got to step 8. Dec 18 comment Propositional formulas 3 It does associate in the sense that for whatever truth value ((A↔B)↔C) has, (A↔(B↔C)) has the same truth value also.