Zulip Chat Archive

Stream: general

Topic: De Morgan's


view this post on Zulip Ken Lee (Oct 22 2018 at 22:10):

Just proved ¬(PQ)¬P¬Q\neg (P \lor Q ) \iff \neg P \land \neg Q and ¬P¬Q¬(PQ)\neg P \lor \neg Q \to \neg (P \land Q) in Lean. I don't see why the converse would require classical logic though. Can someone please explain?

view this post on Zulip Ken Lee (Oct 22 2018 at 22:11):

Just proved $$\not (P \and Q ) \iff \not P \and \not Q$$ and $$\not P \or \not Q \to \not (P \and Q)$$ in Lean. I don't see why the converse would require classical logic though. Can someone please explain?

Oh no. It didn't format the inline maths.

view this post on Zulip Kenny Lau (Oct 22 2018 at 22:12):

¬(PQ)¬P¬Q\neg (P \land Q ) \iff \neg P \land \neg Q and ¬P¬Q¬(PQ)\neg P \lor \neg Q \to \neg (P \land Q)

view this post on Zulip Kenny Lau (Oct 22 2018 at 22:12):

\neg (P \land Q ) \iff \neg P \land \neg Q$$ and $$\neg P \lor \neg Q \to \neg (P \land Q)

view this post on Zulip Ken Lee (Oct 22 2018 at 22:13):

¬(PQ)¬P¬Q\neg (P \land Q ) \iff \neg P \land \neg Q and ¬P¬Q¬(PQ)\neg P \lor \neg Q \to \neg (P \land Q)

Thanks!

view this post on Zulip Jean Lo (Oct 22 2018 at 22:40):

related question: more generally, how does one go about determining whether a proof can be done constructively?

view this post on Zulip Chris Hughes (Oct 22 2018 at 22:43):

If it implies excluded middle then it can't be done constructively. There's an exercise somewhere proving a whole load of things imply excluded middle.

view this post on Zulip Kenny Lau (Oct 22 2018 at 22:45):

but that is not necessary.

view this post on Zulip Kenny Lau (Oct 22 2018 at 22:46):

you can't check every Kripke model though... is there some finite subset that we can check

view this post on Zulip Mario Carneiro (Oct 22 2018 at 22:51):

there is a completeness result that says any intuitionistically invalid statement is false on a finite kripke model

view this post on Zulip Kenny Lau (Oct 22 2018 at 22:52):

that makes set of intuitionstically valid theorems a Π1 set, thus a Δ1 set?

view this post on Zulip Mario Carneiro (Oct 22 2018 at 22:53):

yes, so it is decidable

view this post on Zulip Kevin Buzzard (Oct 22 2018 at 22:53):

@Jean Lo Here is a basic strategy for checking that various simple things can't be done constructively. First observe that all the rules of constructive logic apply when "truth values" are...something like...open sets in a topological space (I hope I remembered this right). You model "not" as "interior of the complement" and "implies" as "is a subset of". Then some stuff like "P or not P" simply isn't true in this interpretation, because the union of an open set and the interior of its complement might not be the whole space.

view this post on Zulip Kenny Lau (Oct 22 2018 at 22:54):

does this together with the 14-theorem give you a fast(er) way of determining stuff?

view this post on Zulip Kenny Lau (Oct 22 2018 at 22:54):

https://en.wikipedia.org/wiki/Kuratowski%27s_closure-complement_problem

view this post on Zulip Mario Carneiro (Oct 22 2018 at 22:54):

It's not complete, unfortunately

view this post on Zulip Mario Carneiro (Oct 22 2018 at 22:54):

at least not unless you consider all topologies

view this post on Zulip Kevin Buzzard (Oct 22 2018 at 22:55):

I don't know, but I don't know what a Kripke model is and yet I've used this way of thinking about things to convince myself that certain propositions can't be proved in classical logic and basically it's the only way I know to do such a thing.

view this post on Zulip Kenny Lau (Oct 22 2018 at 22:55):

just consider the Kuratowski algebra?

view this post on Zulip Mario Carneiro (Oct 22 2018 at 22:57):

A Kripke model is based on a kind of epistemological interpretation of the formulas. There are a bunch of points called "worlds", and at each point there are things that are known to be true at that world, but the things that are not known to be true are just unknowns. There is a "in the future" accessibility relation to other worlds where more things may be known (but previously known things are still known), and things are known to be false only if they are never known in the future

view this post on Zulip Kenny Lau (Oct 22 2018 at 22:58):

I don't think Kevin cares

view this post on Zulip Mario Carneiro (Oct 22 2018 at 22:58):

For example, suppose we have time 0 and time 1, and at time 0 nothing is known and at time 1 pp is known. Then at time 0 neither pp or ¬p\neg p is known

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:01):

This semantics generalizes nicely to modal logic as well, where A\Box A means A is known now and henceforth in the future

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:02):

\square \square

view this post on Zulip Scott Olson (Oct 22 2018 at 23:02):

My intuition regarding ¬(p ∧ q) → ¬p ∨ ¬q is that, as my assumption, I know "p and q aren't both true", but I don't know which one is false, and the conclusion requires me to pick one of the two and prove it's false, which I cannot do

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:03):

ah, is that the program interpretation

view this post on Zulip Scott Olson (Oct 22 2018 at 23:05):

yeah, interpreting as a pair type and as a sum type

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:05):

I think the corresponding model is where at time 0 nothing is known, at time 1a we know q, and at time 1b we know p.

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:06):

The kripke model for this one has three points, with time 0 where nothing is known and a branching future. In world 1, p is known, and in world 2 q is known. Then since pqp\land q is true in no world, ¬(pq)\neg(p\land q) is true in every world, but neither ¬p\neg p nor ¬q\neg q is true in world 0

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:06):

:)

view this post on Zulip Scott Olson (Oct 22 2018 at 23:07):

Interesting, I've never heard of that stuff but it lines up really well with what I did in my head

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:07):

I think you can consider the more general ((p ∧ q) → r) → (p → r) ∨ (q → r) and use the same model

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:08):

yes

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:08):

cool

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:08):

There is no single finite model complete for intuitionistic logic though, or equivalently there is an infinite family of truth values over one proposition

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:08):

or maybe "truth values" just don't make sense

view this post on Zulip Scott Olson (Oct 22 2018 at 23:08):

h : (p ∧ q) → false
⊢ (p → false) ∨ (q → false)

(expanding the \not to the function to false)

I can either assume p or assume q (the two worlds) and then prove false, but I can't apply the function h with just one of them

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:09):

https://upload.wikimedia.org/wikipedia/commons/5/5c/Rieger-Nishimura.svg

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:09):

what is thsi

view this post on Zulip Reid Barton (Oct 22 2018 at 23:09):

I saw this image for the first time like three days ago and I was very confused about how I had never seen it before

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:09):

it is the lattice of propositions over one variable

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:09):

up to equivalence

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:10):

in classical logic it is much less interesting, <p,¬p<\bot < p,\neg p < \top

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:10):

interesting

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:11):

the program interpretation is to let p to mean X contains 1 and q to mean X contains no 1 where X is an arbitrary (computable) binary sequence, right?

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:12):

that's one way to do it

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:14):

But if you like the program (aka BHK) formulation of intuitionistic semantics, then you might like the computational interpretation of peirce's law as call with continuation

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:14):

I never understood what call/cc means

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:18):

The type is callcc : ((p -> q) -> p) -> p. Suppose we are building something of type N, say, and in the course of it we want to do double negation elimination on some proposition p, like say "this TM halts". Then that means we are going to do something with this value of type p, so that's a function p -> N, and so callcc steals this "continuation" and passes it to the enclosed function of type (p -> N) -> p

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:34):

For example, consider the following implementation of em:

constant callcc {p q : Type} : ((p -> q) -> p) -> p

def em (p : Type) : p  (p  empty) :=
@callcc _ empty $ λ H,
show p  (p  empty), from sum.inr $ λ hp, H $
show p  (p  empty), from sum.inl hp

This function looks like magic when you see it for the first time. It's a computational interpretation of EM! So we can just put in our favorite nondecidable proposition to this oracle, like the Riemann hypothesis, and find out the answer. It calls callcc at this point, which remembers our position in the code, and then calls the sum.inr constructor. So the oracle says: RH is false! We are happy until we find out maybe that RH is actually true, and in justified anger return to our function to prove a contradiction. When we call the function though, it calls H with sum.inl hp. What happened? The function H remembers when we called callcc the first time, and "rewinds time" with our proof of RH in hand. So the oracle says: RH is true! and it stole our proof.

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:39):

our favorite nondecidable proposition to this oracle, like the Riemann hypothesis

hmm...

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:41):

I guess this is like "innocent until proven guilty", we have "false until proven true"

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:41):

I still don't understand what it does... thanks for your lengthy explanation though

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:41):

The semantics is a bit tricky to explain without a notion of "continuation"

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:42):

the idea is that every expression exists in a context, where you are evaluating an expression in order to pass it to something else

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:42):

and this something else can be thought of as a function from the type of the expr to the "final output"

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:42):

which can be whatever, it doesn't really matter

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:43):

it's like an expression with a hole in it where our expr goes

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:43):

and callcc saves this expr-with-hole that surrounds the callcc f expression itself, and calls f on it

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:45):

This enables bizarre behavior like returning twice from a function or functions that call each other as coroutines, or exception handling

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:45):

lots of control flow can be expressed using continuations

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:47):

what kind of thing is call/cc?

view this post on Zulip Kenny Lau (Oct 22 2018 at 23:47):

is it a function that we can implement? is it a function that only exists in some alternate programming language?

view this post on Zulip Mario Carneiro (Oct 23 2018 at 00:21):

it isn't a function you can implement in lean, but it is a function that could conceivably be supported in the VM as a primitive

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:19):

Could you write your RH thing in say Scheme?

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:24):

yes

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:24):

I think they are the pioneers of callcc

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:26):

then what would it return?

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:27):

like I said, "false" until you prove it wrong

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:27):

and then it goes back in time with your proof and says "true"

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:28):

do you have actual Scheme code?

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:28):

no, but you should just be able to use callcc in a term like I've shown

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:29):

the lean code should translate without issue to scheme

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:30):

there is also the matter of scheme not being a typed language

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:34):

if the time travel is the part that is surprising, a more pedestrian explanation is that it just saves the current state of the VM - the call stack and values of the variables, then we can later "reset" to this execution state

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:35):

how does the program "take" our proof?

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:35):

you pass it to the function in an attempt to derive false

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:36):

and rather than producing a proof of false, it abandons the entire execution of the rest of the program and resets with this proof in hand

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:37):

does callcc have any equational lemmas?

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:37):

yes, but they are a bit weird because they depend on the execution context

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:42):

You have to set up the idea of a dynamic semantics. Let's say we want to evaluate e1 + e2, we can write this as e1 + e2 < Kwhere K is the call stack. It is expecting a value of type nat say, here. So we first evaluate e1, that is, e1 < _ + e2, K where we have pushed _ + e2 on the stack. We get to a value v > _ + e2, K (the arrow is reversed to indicate that the value is done computing) which steps to e2 < v + _, K. That is we are evaluating e2 now. This finishes to v2 > v + _, K which steps to v' > K where v' is the actual result of adding numbers v and v2

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:42):

I don't understand how you can pass the proof to the function

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:42):

the function doesn't accept things of type p right

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:42):

it wants a thing of type (p -> q) -> p

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:43):

In the em example I define a particular function of type (p -> false) -> p

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:43):

or rather (p + not p -> false) -> p + not p

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:44):

so when the callcc is called it evaluates this function giving it a kind of magic function which has type p + not p -> false

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:46):

this function should not ever be called, because it "destroys the universe" rather than producing a proof of false

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:50):

Here's another example. If f : (N -> false) -> N is the constant function 42, then callcc f just returns 42. Nothing special happens as long as f never uses its argument

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:51):

But if f = \lam g, false.elim (g 12), then callcc f returns 12

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:51):

how?

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:52):

and if f = \lam g, false.elim (g 12) + false.elim (g 13)?

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:52):

returns 12

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:53):

the rest of the computation is abandoned once g is called

view this post on Zulip Kenny Lau (Oct 23 2018 at 06:53):

hmm...

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:53):

The function g given to f is actually the expr-with-hole that callcc f is situated in

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:55):

it might make more sense if g is called throw instead

view this post on Zulip Mario Carneiro (Oct 23 2018 at 06:55):

and callcc is catch


Last updated: May 06 2021 at 22:13 UTC