Garry G wrote: ↑Sun Apr 14, 2019 2:49 pm
Ok I don't code so the syntax is strange to me.
I think this says something alone the lines of:
a ⇒ b ⊨ ¬(a) ⋁ b
q ⊨ (p ⋀ q) ⇒ p
I am not sure why we move from the lower case a, b to p, q. but I think you defined implication with the lower case letters. I don't know what the stuff about a toggle means.
It doesn't matter - they are just temporary variables. I can rename them to p and q. It will do the same thing.
Garry G wrote: ↑Sun Apr 14, 2019 2:49 pm
but clearly p & q => p is a theorem and so the argument ought to be true, and it is recognised as mistake if a program returns false.
Recognized by whom and why?
The problem of "define error" or "define a mistake" boils all the way up to human ethics. "Right" and "wrong".
This is where we will diverge. You treat logic as prescriptive and axioms of logic as laws. I don't. They are arbitrary choices.
They may be useful axioms. Useful to somebody and in some context, but I am free to reject them as and when it suits me if they get in my way.
The key thing to see here is that axioms are the product of arbitrary choice. And in turn - the theorems that result are the consequences of the axiom that you've chosen.
If I choose a different axiom - I will get different theorems.
Garry G wrote: ↑Sun Apr 14, 2019 2:49 pm
this is my understanding: the program arrives at the wrong answer because the programmer has failed to make two inputs mutually exclusive. And one slower signal just fails to get there in time to cancel the other signal.
Now look where you have ended up. You are already claiming that you know what the "right" answer is.
If you already know the truth - what do you need logic for?
The most important development in logic in the last 100 years is the
Curry-Howard correspondence
It says that a mathematical proof is the same beast as a computer algorithm.
And so in a constructivist paradigm p and q are objects. ANY mathematical objects. That behave in any way you can imagine them behaving.
And this statement is nothing more than a proposition: p & q => p
IF I can find values for p and q such that the above evaluates to "true" then that is proof for your claim.
Garry G wrote: ↑Sun Apr 14, 2019 2:49 pm
I'm assuming that his kind of problem is not just down to bad circuit design and bad programming. If it is just bad design then my answer is the same as the picture of the tank and pipe. The design is fixable.
The design is fixable. Logic is not.
Logic is not what you think it is. It's not a source of truth. It's a framework for computation.
Garry G wrote: ↑Sun Apr 14, 2019 2:49 pm
This is not a logical problem and the logical principles are not in any danger.
What would you say the "logical principles" are?
Identity? x = x ⇔ True
I can (have) constructed systems where it evaluates to False.
non-contradiction? (p & ~p) ⇔ False
I can (have) constructed logical systems where it evaluates to True.
Axioms.... All axioms are arbitrary.
Aristotelian logic is dead. Church and Turing killed it.