Questions about analysis of proofs in theories

learn more… | top users | synonyms

1
vote
0answers
60 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 ...
6
votes
0answers
58 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 ...
8
votes
2answers
714 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 ...
6
votes
2answers
231 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 ...
3
votes
2answers
176 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 ...
1
vote
2answers
90 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$? ...
13
votes
3answers
529 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 ...
11
votes
2answers
710 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 ...
3
votes
1answer
187 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 ...
8
votes
1answer
154 views

Unification-based elimination rule for equality

A few years back, I ran across the following left-rule for equality in sequent calculus: $$ \frac{s \doteq t \leadsto \theta \qquad \theta(\Gamma) \vdash \theta(C)} {\Gamma, s \doteq t ...
4
votes
1answer
176 views

Resolution vs Extended Resolution

Let $R(f)$ and $ER(f)$ be the minimum-size for unsat proofs of $f$ in Resolution and Extended Resolution respectively. What's the best bound we have on $D=\min_f (R(f)-ER(f))$ where $f$ belongs to a ...
12
votes
1answer
252 views

Barendregt's proof of subject reduction for $\lambda2$

I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types). The last step of the proof (page 60), says: "and hence by Lemma 4.1.19(1), ...
13
votes
3answers
488 views

Can we prove weak normalization for System F by induction on a transfinite ordinal

Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
6
votes
1answer
138 views

converse relationship between the cut rule and the identity axiom

On page 30 of "Proofs and Types" by Girard, Taylor, and Lafont, it is claimed that that the identity axiom for sequent calculus: C ├ C has a converse relation with the cut rule: $$\frac{\vec{A} ...
26
votes
1answer
768 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 ...
11
votes
2answers
278 views

References to programming languages based on conditional logics

Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; ...
14
votes
1answer
318 views

Looking for papers and articles on the Tarskian Möglichkeit

Some background: Łukasiewicz many-valued logics were intended as modal logics, and Łukasiewicz gave an extensional definition of the modal operator: $\Diamond A =_{def} \neg A \to A$ (which he ...
18
votes
1answer
617 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 ...
17
votes
3answers
896 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 ...
8
votes
3answers
184 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 ...
27
votes
3answers
1k 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 ...
8
votes
2answers
312 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) ...
12
votes
1answer
353 views

Are innermost reductions perpetual in untyped λ-calculus?

(I have already asked this at MathOverflow, but got no answers there.) Background In the untyped lambda calculus, a term may contain many redexes, and different choices about which one to reduce may ...
11
votes
2answers
335 views

What happens if we try to extract a witness but it actually does not exist from a term of existential type?

Given a term t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y)) in Martin-Lof's type theory, what's the value of w(t(0)), where ...