Fdtxjr

Is there a kind of relay only consumes power when switching?

Selecting user stories during sprint planning

Significance of Cersei's obsession with elephants?

How does the math work when buying airline miles?

How to react to hostile behavior from a senior developer?

Do wooden building fires get hotter than 600°C?

A term for a woman complaining about things/begging in a cute/childish way

Generate an RGB colour grid

How do I use the new nonlinear finite element in Mathematica 12 for this equation?

Why should I vote and accept answers?

What's the meaning of "fortified infraction restraint"?

Drawing without replacement: why is the order of draw irrelevant?

Should I follow up with an employee I believe overracted to a mistake I made?

What is a fractional matching?

How often does castling occur in grandmaster games?

How do living politicians protect their readily obtainable signatures from misuse?

Why does it sometimes sound good to play a grace note as a lead in to a note in a melody?

Can anything be seen from the center of the Boötes void? How dark would it be?

AppleTVs create a chatty alternate WiFi network

Find 108 by using 3,4,6

Using et al. for a last / senior author rather than for a first author

Sum letters are not two different

How to compare two different files line by line in unix?

What do you call the main part of a joke?

Does the order of applying rules in Sequent Calculus matter?

1

$begingroup$

Suppose we want to prove some $Gamma models Delta$ in (first-order logic) sequent calculus LK.
We start with the sequent $Gamma vdash Delta$, and arbitrarily apply rules backward until we reach sequents that only contain atomic formulae. Then, either the sequents are axioms (e.g. $A vdash A$), or not (e.g. $A vdash B$).

Now, suppose that $Gamma models Delta$. If we apply rules arbitrarily, are we guaranteed to always end up with axioms ($A vdash A$)? Or can the order of application of rules change that outcome?

Another way of asking this: If at some point in the derivation we see a sequent with only atoms that is not an axiom (e.g. $A vdash B$), can we immediately infer that $Gamma notmodels Delta$?

Is the outcome different if $Gamma models Delta$ would only contain propositions, no predicates?

Thanks for the help :)

PS: Maybe this was a little unclear... Both $Gamma$ and $Delta$ can be one or more well-formed formulae.

first-order-logic proof-theory sequent-calculus

share|cite|improve this question

edited Mar 27 at 16:17

Rafael Bankosegger

asked Mar 27 at 16:03

Rafael BankoseggerRafael Bankosegger

696

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Basically, the order is deterministic. Rules act on a single connective or quantifier at the time and we can apply a rule only to the principal connective. I.e. The formula $p to (q land r)$ can be decomposed only with the rule for $to$.
  $endgroup$
  – Mauro ALLEGRANZA
  Mar 27 at 16:12
  
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  I would disagree. You most of the time have at least two choices: Apply a rule on the left side of the sequent, or on the right. Also, there might be different rules that apply.For example, the exchange / weakening rules apply in most cases.
  $endgroup$
  – Rafael Bankosegger
  Mar 27 at 16:15
  
  

  
  
  
  

add a comment | 

1

$begingroup$

Suppose we want to prove some $Gamma models Delta$ in (first-order logic) sequent calculus LK.
We start with the sequent $Gamma vdash Delta$, and arbitrarily apply rules backward until we reach sequents that only contain atomic formulae. Then, either the sequents are axioms (e.g. $A vdash A$), or not (e.g. $A vdash B$).

Now, suppose that $Gamma models Delta$. If we apply rules arbitrarily, are we guaranteed to always end up with axioms ($A vdash A$)? Or can the order of application of rules change that outcome?

Another way of asking this: If at some point in the derivation we see a sequent with only atoms that is not an axiom (e.g. $A vdash B$), can we immediately infer that $Gamma notmodels Delta$?

Is the outcome different if $Gamma models Delta$ would only contain propositions, no predicates?

Thanks for the help :)

PS: Maybe this was a little unclear... Both $Gamma$ and $Delta$ can be one or more well-formed formulae.

first-order-logic proof-theory sequent-calculus

share|cite|improve this question

edited Mar 27 at 16:17

Rafael Bankosegger

asked Mar 27 at 16:03

Rafael BankoseggerRafael Bankosegger

696

$endgroup$

• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  Basically, the order is deterministic. Rules act on a single connective or quantifier at the time and we can apply a rule only to the principal connective. I.e. The formula $p to (q land r)$ can be decomposed only with the rule for $to$.
  $endgroup$
  – Mauro ALLEGRANZA
  Mar 27 at 16:12
  
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  $begingroup$
  I would disagree. You most of the time have at least two choices: Apply a rule on the left side of the sequent, or on the right. Also, there might be different rules that apply.For example, the exchange / weakening rules apply in most cases.
  $endgroup$
  – Rafael Bankosegger
  Mar 27 at 16:15
  
  

  
  
  
  

add a comment | 

$begingroup$

Suppose we want to prove some $Gamma models Delta$ in (first-order logic) sequent calculus LK.
We start with the sequent $Gamma vdash Delta$, and arbitrarily apply rules backward until we reach sequents that only contain atomic formulae. Then, either the sequents are axioms (e.g. $A vdash A$), or not (e.g. $A vdash B$).

Now, suppose that $Gamma models Delta$. If we apply rules arbitrarily, are we guaranteed to always end up with axioms ($A vdash A$)? Or can the order of application of rules change that outcome?

Another way of asking this: If at some point in the derivation we see a sequent with only atoms that is not an axiom (e.g. $A vdash B$), can we immediately infer that $Gamma notmodels Delta$?

Is the outcome different if $Gamma models Delta$ would only contain propositions, no predicates?

Thanks for the help :)

PS: Maybe this was a little unclear... Both $Gamma$ and $Delta$ can be one or more well-formed formulae.

first-order-logic proof-theory sequent-calculus

share|cite|improve this question

edited Mar 27 at 16:17

Rafael Bankosegger

asked Mar 27 at 16:03

Rafael BankoseggerRafael Bankosegger

696

$endgroup$

share|cite|improve this question

edited Mar 27 at 16:17

Rafael Bankosegger

asked Mar 27 at 16:03

Rafael BankoseggerRafael Bankosegger

696

share|cite|improve this question

edited Mar 27 at 16:17

Rafael Bankosegger

asked Mar 27 at 16:03

Rafael BankoseggerRafael Bankosegger

696

asked Mar 27 at 16:03

Rafael BankoseggerRafael Bankosegger

696

asked Mar 27 at 16:03

Rafael BankoseggerRafael Bankosegger

696