516 reputation
419
bio website
location
age
visits member for 3 years, 9 months
seen Sep 16 at 12:01

Dear All,

If you want raw timely information about what is cooking in our lab you can follow the following Google+ and Twitter streams:

Google+ Jekejeke Prolog
Twitter Jekejeke Prolog

We have discontinued our Facebook, Linkedin and XING accounts and are now exclusively posting on Google+ and Twitter.

Have Fun


Aug
23
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
Dec
29
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.
Sep
25
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.
Sep
23
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.
Sep
23
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).
Sep
23
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?
Sep
22
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.
Aug
22
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.
Aug
22
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?
Aug
22
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?
Aug
22
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.
Aug
22
comment logic question: enumerating propositions
How about HOL with some general semantics? Not the full semantic?
Jun
11
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?)
Jun
11
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.
Apr
26
comment Less absorption in Minimal Logic?
Yes, sounds good!
Apr
26
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?
Apr
26
comment Less absorption in Minimal Logic?
This is a kind of a tex challenge for me.
Apr
26
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?
Jan
11
comment Antique handling of consequentia mirabilis?
@PeterSmith sorry, my fault. Was thinking in terms of minimal logic where one additionally assumes /A = A -> f.
Jan
11
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?