I'm reading Barendregt's Lambda calculi with types (1992). In Proposition 184.108.40.206., he "proves" a lemma which shows the approximation rule implies the equality rule in typed lambda-calculi à la ...
I'm wondering why we can't express graph reachability in first order logic in pretty much exactly the same way we express it in second order existential logic. For SOL, one definition is : 1 . L is ...
I'm reading the seminal "Monitors" paper by Hoare. On page 4 he proceeds with a logical proof using syntax I've never seen before, and neither know what it's called or how to properly read it. ...
I study computer science at a university. My school offers several courses where various proofs are expected, but there is no course that introduces the fundamental concepts of proofs and how to write ...
My question can be read on many levels and so I welcome answers to any reading. The general question is: What is the computational complexity of verifying a proof? One way of looking at a ...
From Scott Aaronson's blog: There’s a finite (and not unimaginably-large) set of boxes, such that if we knew how to pack those boxes into the trunk of your car, then we’d also know a proof ...