Reputation
6,141
Top tag
Next privilege 10,000 Rep.
Access moderator tools
Badges
13 37
Impact
~207k people reached

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.