less info
reputation
419
bio website location age member for 3 years, 9 months seen Sep 16 at 12:01 profile views 354

Dear All,

 Aug23 comment Using $p\supset q$ instead of $p\implies q$ It is rather the other way around. From residuated lattices we know p≤q->r iff p^q≤r. Now take the special case p=1, we then have q->r iff q≤r. en.wikipedia.org/wiki/Residuated_lattice Dec29 comment Why is 'abuse of notation' tolerated? Without further research you are saying that I were using non-standard notation. May I show you the following reference: ISO 31-11: ⇒ p ⇒ q implication sign if p then q; p implies q Can also be written as q ⇐ p. Sometimes → is used. en.wikipedia.org/wiki/ISO_31-11 . Seems you are suffering from some severe self overestimates, the only thing that is distracting here. Sep25 comment What are the historical roots of cryptarithmetic? This is a hukumenzan: janko.at/Raetsel/Nikoli/Hukumenzan.htm . Somebody told me the translation is "prune and peach are friends", and the script is Hiragana. Sep23 comment What are the historical roots of cryptarithmetic? Looks they are called nowadays hukumenzan in Japan. But how about China? I still don't know. Sep23 comment Induction, how often? I have constructed the example from the property that ∀x doesn't preserve countable infinite ascending unions. The existential quantifier does so. But I am not yet sure what the implications are for induction. Maybe one can construct a predicate q, prove it by a single induction, and then derive p. Like following the odd numbers and hypothetically following the even numbers at the same time, and joining the two together resolving the hypothesis. The hypothesis would be p(1). Sep23 comment Induction, how often? Greetings from CH to CH. Looks like an agreement that ∀x p(x) holds. But somehow the proof doesn't go through with a single induction over p, does it? Sep22 comment Why does the expression of Peano induction has to be second order? Actually first order induction means that one adds a schema. So the X is really quantified, but not in the object logic but syntactically on the meta-level. Aug22 comment What kind of logics satisfy the coincidence lemma? Then the truth can depend on more than only p and x. For example if I substitute f(y) for x, and in one case a for y and in another case b for y. I could get different truth values. Aug22 comment What kind of logics satisfy the coincidence lemma? Take p(x). Usually the truth value of the above sentence only depends on the interpretation of p and the domain value of x. But what if we allow to determine the truth to perform simultaneous non-ground substitutions? Aug22 comment What kind of logics satisfy the coincidence lemma? If sigma is not an interpretation, but a simultaneous non-ground substitution, then the lemma doesn't hold. Right? Is there some logic that would amount to that? Aug22 comment What kind of logics satisfy the coincidence lemma? Yeah, possibly we could define occuring free in A after the fact semantically and not before the fact syntactically, by virtue of this lemma. Aug22 comment logic question: enumerating propositions How about HOL with some general semantics? Not the full semantic? Jun11 comment Predicate equivalence from Horn clauses? I would say lfp <> Universe, i.e. a non-trivial least fixpoint is sufficient and also necessary. (Hope lfp is always defined as a concept, can we get it via set theory?) Jun11 comment Predicate equivalence from Horn clauses? n is a FOL constant. X is a FOL variable. even and even' are FOL predicates of arity 1. s is a FOL function of arity 1. There are no further definitions around that would involve n or s. Apr26 comment Less absorption in Minimal Logic? Yes, sounds good! Apr26 comment Less absorption in Minimal Logic? So you assume inversion for conjunction, i.e. if A |- B /\ C, then A |- B and A |- C? To make the argument go through? Apr26 comment Less absorption in Minimal Logic? This is a kind of a tex challenge for me. Apr26 comment Less absorption in Minimal Logic? Now the comment /* not derivable */ is gone, and it looks as I state something true. Can this comment be restored in math? Jan11 comment Antique handling of consequentia mirabilis? @PeterSmith sorry, my fault. Was thinking in terms of minimal logic where one additionally assumes /A = A -> f. Jan11 comment Antique handling of consequentia mirabilis? Yes, the natural deduction formulation does the same. Any particular reason to use /A instead of ~A? Is this historical more adequate?