# Tagged Questions

Questions about analysis of proofs in theories

87 views

### Is there any work relating type systems and Cook-Reckhow proof systems?

An important subfield of computational complexity is proof complexity, mostly due to Cook and Reckhow. E.g. one notable result is that a proof system that has efficient proofs (i.e., in length ...
561 views

### Why is Proof Checker required in Proof Carrying Code

In the classical PLDI'98 paper by Necula, "The design and implementation of a certifying compiler", the high-level verifier uses: VCGen to generate verification conditions (safety predicates) First-...
98 views

### Undecidable Single Programs [closed]

So the halting problem basically states that there cannot exist any finite length algorithm for automatically verifying if other finite length algorithms terminate. But suppose I start listing out ...
496 views

### Why do constructivists not seem to care too much about call/cc

So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't ...
120 views

### About the position of side conditions in an inference rule

Sometimes I see people put side conditions above the inference line as if they were premises of an inference rule. This feels strange. My understanding (which may be wrong) is that a side condition ...
106 views

### Hypersequents: proof term assigments or translations to hybrid logic

I've been looking at a modal logic with the axiom $$(\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B))$$ Roughly, this says that the ...
800 views

### Turing machines whose termination is unprovable?

I have a naive question: does there exist a Turing machine whose termination is true but unprovable by any natural, consistent and finitely axiomatizable theory? I ask for a mere existence proof ...
251 views

### SAT in some DTIME always via a constructive proof?

Why can the statement $SAT \in DTIME(n^3)$ not be proven through a non-constructive proof? Intuitively a proof would be a turing machine, which solves this problem in $DTIME(n^3)$, but there are non-...
250 views

### Derivation of cut rule in sequent calculus

I searched internet but could not find any good weblink which shows how the cut rule for sequent calculus can be derived. I found this paper but it uses implication elimination rule which I cannot ...
100 views

### Is there an $\mathcal{L}$-theory and a formula $\phi$ for which Kolmogorov(proof($\phi$)) $<$ Kolmogorov($\phi$)?

Are there a complete decidable $\mathcal{L}$-theory, a formula $\phi$ and a proof of $\phi$ for which the Kolmogorov complexity of the proof of $\phi$ is less than the Kolmogorov complexity of $\phi$? ...
672 views

### funsplit and polarity of Pi-types

In a recent thread on the Agda mailing list, the question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark. My understanding is that $\eta$ laws come with negative ...
1k views

### Is propositional resolution a complete proof system?

This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution". This question is something extremely basic but it has been bothering me ...
207 views

### Why is there a need for cyclic proofs?

I was reading a paper A Generic Cyclic Theorem Prover. This paper explains about automated theorem prover based on various instantiations like the notion of first order logic equations with inductive ...
202 views

802 views

### Inductive types for large countable ordinal notations.

I'm looking to build notations for large countable ordinals in a "natural way". By "natural way" I mean that given an inductive data type X, that equality should be the usual recursive equality (the ...
299 views

800 views

### Are types propositions? (What are types exactly?)

I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in ...
2k views

### How would I go about learning the underlying theory of the Coq proof assistant?

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
189 views

### Looking for papers and articles on higher-order sequent systems

I am looking for work on systems that are similar to K. Dosen's higher-order sequents ("Sequent Systems for Modal Logic", JSL 50). The only work that I am aware of is recent work by Iemhoff and ...
526 views

### Looking for papers and articles on modal substructural logics

I am looking for papers and articles on modal substructural logics-- not on the semantics of linear logic modalities, but on substructural logics augmented with standard modal operators, e.g. ...
2k views

### Curry-Howard and programs from non-constructive proofs

This is a follow up question to What is the difference between proofs and programs (or between propositions and types)? What program would correspond to a non-constructive (classical) proof of the ...
319 views

### About the correspondence of left introduction and elimination of implication in Sequent Calculus and in Natural Deduction resp.

Could anyone give an intuitive (not intutionistic) explanation of the correspondence of left introduction and elimination of implication in Sequent Calculus (SC) and Natural Deduction (ND) ...