Misplaced Pages

#80919

74-403: Admissibility has been systematically studied only in the case of structural (i.e. substitution -closed) rules in propositional non-classical logics , which we will describe next. Let a set of basic propositional connectives be fixed (for instance, { → , ∧ , ∨ , ⊥ } {\displaystyle \{\to ,\land ,\lor ,\bot \}} in

148-413: A {\textstyle a} and b {\textstyle b} , and any well-formed formula ϕ ( x ) {\textstyle \phi (x)} (with a free variable x). For example: For all real numbers a and b , if a = b , then a ≥ 0 implies b ≥ 0 (here, ϕ ( x ) {\displaystyle \phi (x)} is x ≥ 0 ). This

222-414: A i = a 1 ∧ a 2 ∧ … a n − 1 ∧ a n {\displaystyle \bigwedge _{i=1}^{n}a_{i}=a_{1}\wedge a_{2}\wedge \ldots a_{n-1}\wedge a_{n}} In classical logic , logical conjunction is an operation on two logical values , typically the values of two propositions , that produces

296-417: A i k {\textstyle \sum _{i<k}a_{ik}} , depending on the context, the variable i {\textstyle i}  can be free and k {\textstyle k} bound, or vice-versa, but they cannot both be free. Determining which value is assumed to be free depends on context and semantics . The substitution property of equality , or Leibniz's Law (though

370-448: A Kripke model M = ⟨ W , R , ⊩ ⟩ {\displaystyle M=\langle W,R,{\Vdash }\rangle } by Then the following provides an algorithmic criterion for admissibility in K 4: Theorem . The rule ⋁ i = 0 n φ i / p 0 {\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}}

444-404: A formal language , a variable is a symbol from an alphabet , usually a letter like x , y , and z , which denotes a range of possible values . If a variable is free in a given expression or formula , then it can be replaced with any of the values in its range. Certain kinds of bound variables can be substituted too. For instance, parameters of an expression (like the coefficients of

518-501: A polynomial ), or the argument of a function . Moreover, variables being univerally quantified can be replaced with any of the values in its range, and the result will a true statement . (This is called Universal instantiation ) For a non-formalized language, that is, in most mathematical texts outside of mathematical logic , for an individual expression it is not always possible to identify which variables are free and bound. For example, in ∑ i < k

592-474: A few trivial cases, frames with tight predecessors must be infinite. Hence admissible rules in basic transitive logics do not enjoy the finite model property. While a general classification of structurally complete logics is not an easy task, we have a good understanding of some special cases. Intuitionistic logic itself is not structurally complete, but its fragments may behave differently. Namely, any disjunction-free rule or implication-free rule admissible in

666-407: A finite or independent basis of rules. Finite bases are relatively rare: even the basic transitive logics IPC , K 4, S 4, GL , Grz do not have a finite basis of admissible rules, though they have independent bases. A rule Γ/ B is valid in a modal or intuitionistic Kripke frame F = ⟨ W , R ⟩ {\displaystyle F=\langle W,R\rangle } , if

740-500: A given logic is whether the set of all admissible rules is decidable . Note that the problem is nontrivial even if the logic itself (i.e., its set of theorems) is decidable : the definition of admissibility of a rule A / B involves an unbounded universal quantifier over all propositional substitutions. Hence a priori we only know that admissibility of rule in a decidable logic is Π 1 0 {\displaystyle \Pi _{1}^{0}} (i.e., its complement

814-406: A ground substitution is a ground term if all of t ' s variables are in σ ' s domain, i.e. if vars ( t ) ⊆ dom ( σ ). A substitution σ is called a linear substitution if tσ is a linear term for some (and hence every) linear term t containing precisely the variables of σ ' s domain, i.e. with vars ( t ) = dom ( σ ). A substitution σ is called a flat substitution if xσ

SECTION 10

#1732772272081

888-453: A recursive or finite basis of admissible rules, and to provide an explicit basis. If a logic has no finite basis, it can nevertheless have an independent basis : a basis R such that no proper subset of R is a basis. In general, very little can be said about existence of bases with desirable properties. For example, while tabular logics are generally well-behaved, and always finitely axiomatizable, there exist tabular modal logics without

962-477: A rule A 1 , … , A n / B {\displaystyle A_{1},\dots ,A_{n}/B} is equivalent to A 1 ∧ ⋯ ∧ A n / B {\displaystyle A_{1}\land \dots \land A_{n}/B} with respect to admissibility and derivability. It is therefore customary to only deal with unary rules A / B . The basic question about admissible rules of

1036-408: A rule may include the use of a substitution instance for the purpose of introducing certain variables into a derivation. A propositional formula is a tautology if it is true under every valuation (or interpretation ) of its predicate symbols. If Φ is a tautology, and Θ is a substitution instance of Φ, then Θ is again a tautology. This fact implies the soundness of the deduction rule described in

1110-407: A substitution σ that unifies A but not B , and one for a derivation of A / B from R and ⊢ L {\displaystyle \vdash _{L}} . One of the searches has to eventually come up with an answer.) Apart from decidability, explicit bases of admissible rules are useful for some applications, e.g. in proof complexity . For a given logic, we can ask whether it has

1184-499: A substitution σ to a term t is called an instance of that term t . For example, applying the substitution { x  ↦  z , z  ↦  h ( a , y ) } to the term The domain dom ( σ ) of a substitution σ is commonly defined as the set of variables actually replaced, i.e. dom ( σ ) = { x ∈ V | xσ ≠ x }. A substitution is called a ground substitution if it maps all variables of its domain to ground , i.e. variable-free, terms. The substitution instance tσ of

1258-414: A superintuitionistic logic L with its standard consequence relation ⊢ L {\displaystyle \vdash _{L}} generated by modus ponens and axioms, and we identify a normal modal logic with its global consequence relation ⊢ L {\displaystyle \vdash _{L}} generated by modus ponens, necessitation, and (as axioms) the theorems of

1332-637: A superintuitionistic logic is derivable. On the other hand, the Mints rule is admissible in intuitionistic logic but not derivable, and contains only implications and disjunctions. We know the maximal structurally incomplete transitive logics. A logic is called hereditarily structurally complete , if any extension is structurally complete. For example, classical logic, as well as the logics LC and Grz .3 mentioned above, are hereditarily structurally complete. A complete description of hereditarily structurally complete superintuitionistic and transitive modal logics

1406-412: A value of true if and only if (also known as iff) both of its operands are true. The conjunctive identity is true, which is to say that AND-ing an expression with true will never change the value of the expression. In keeping with the concept of vacuous truth , when conjunction is defined as an operator or function of arbitrary arity , the empty conjunction (AND-ing over an empty set of operands)

1480-451: A variant of the disjunction property, the multiple-conclusion rules have the same expressive power as single-conclusion rules: for example, in S 4 the rule above is equivalent to Substitution (logic) A substitution is a syntactic transformation on formal expressions. To apply a substitution to an expression means to consistently replace its variable, or placeholder, symbols with other expressions. The resulting expression

1554-498: Is admissible if for every instance of the rule, σB is a theorem whenever all formulas from σ Γ are theorems. In other words, a rule is admissible if it, when added to the logic, does not lead to new theorems. We also write Γ | ∼ B {\displaystyle \Gamma \mathrel {|\!\!\!\sim } B} if Γ/ B is admissible. (Note that . | ∼ {\displaystyle {\phantom {.}}\!{|\!\!\!\sim }}

SECTION 20

#1732772272081

1628-427: Is less general than an L -unifier τ , written as σ ≤ τ , if there exists a substitution υ such that for every variable p . A complete set of unifiers of a formula A is a set S of L -unifiers of A such that every L -unifier of A is less general than some unifier from S . A most general unifier (MGU) of A is a unifier σ such that { σ } is a complete set of unifiers of A . It follows that if S

1702-456: Is not admissible in K 4 if and only if there exists a set W ⊆ { φ i ∣ i ≤ n } {\displaystyle W\subseteq \{\varphi _{i}\mid i\leq n\}} such that Similar criteria can be found for the logics S 4, GL , and Grz . Furthermore, admissibility in intuitionistic logic can be reduced to admissibility in Grz using

1776-530: Is recursively enumerable ). For instance, it is known that admissibility in the bimodal logics K u and K 4 u (the extensions of K or K 4 with the universal modality ) is undecidable. Remarkably, decidability of admissibility in the basic modal logic K is a major open problem. Nevertheless, admissibility of rules is known to be decidable in many modal and superintuitionistic logics. The first decision procedures for admissible rules in basic transitive modal logics were constructed by Rybakov , using

1850-463: Is a basis if and only if . | ∼ L {\displaystyle {\phantom {.}}\!{|\!\!\!\sim _{L}}} is the smallest structural consequence relation that includes ⊢ L {\displaystyle \vdash _{L}} and R . Notice that decidability of admissible rules of a decidable logic is equivalent to the existence of recursive (or recursively enumerable ) bases: on

1924-428: Is a classically valid , simple argument form . The argument form has two premises, A {\displaystyle A} and B {\displaystyle B} . Intuitively, it permits the inference of their conjunction. or in logical operator notation, where \vdash expresses provability: Here is an example of an argument that fits the form conjunction introduction : Conjunction elimination

1998-442: Is a complete set of unifiers of A , then a rule A / B is L -admissible if and only if every σ in S is an L -unifier of B . Thus we can characterize admissible rules if we can find well-behaved complete sets of unifiers. An important class of formulas that have a most general unifier are the projective formulas : these are formulas A such that there exists a unifier σ of A such that for every formula B . Note that σ

2072-468: Is a ground substitution, { x  ↦  x 1 , y  ↦  y 2 +4 } is non-ground and non-flat, but linear, { x  ↦  y 2 , y  ↦  y 2 +4 } is non-linear and non-flat, { x  ↦  y 2 , y  ↦  y 2 } is flat, but non-linear, { x  ↦  x 1 , y  ↦  y 2 } is both linear and flat, but not a renaming, since it maps both y and y 2 to y 2 ; each of these substitutions has

2146-410: Is a pair (Γ,Δ) of two finite sets of formulas, written as Such a rule is admissible if every unifier of Γ is also a unifier of some formula from Δ. For example, a logic L is consistent iff it admits the rule and a superintuitionistic logic has the disjunction property iff it admits the rule Again, basic results on admissible rules generalize smoothly to multiple-conclusion rules. In logics with

2220-456: Is a property which is most often used in algebra , especially in solving systems of equations , but is apllied in nearly every area of math that uses equality. This, taken together with the reflexive property of equality, forms the axioms of equality in first-order logic. Substitution is related to, but not identical to, function composition ; it is closely related to β -reduction in lambda calculus . In contrast to these notions, however,

2294-425: Is a structural consequence relation on its own.) Every derivable rule is admissible, but not vice versa in general. A logic is structurally complete if every admissible rule is derivable, i.e., ⊢ = | ∼ {\displaystyle {\vdash }={\,|\!\!\!\sim }} . In logics with a well-behaved conjunction connective (such as superintuitionistic or modal logics),

Admissible rule - Misplaced Pages Continue

2368-411: Is a substitution instance of: and is a substitution instance of: In some deduction systems for propositional logic, a new expression (a proposition ) may be entered on a line of a derivation if it is a substitution instance of a previous line of the derivation (Hunter 1971, p. 118). This is how new lines are introduced in some axiomatic systems . In systems that use rules of transformation ,

2442-431: Is a variable for every variable x . A substitution σ is called a renaming substitution if it is a permutation on the set of all variables. Like every permutation, a renaming substitution σ always has an inverse substitution σ , such that tσσ = t = tσ σ for every term t . However, it is not possible to define an inverse for an arbitrary substitution. For example, { x  ↦ 2, y  ↦ 3+4 }

2516-475: Is an MGU of A . In transitive modal and superintuitionistic logics with the finite model property , one can characterize projective formulas semantically as those whose set of finite L -models has the extension property : if M is a finite Kripke L -model with a root r whose cluster is a singleton , and the formula A holds at all points of M except for r , then we can change the valuation of variables in r so as to make A true at r as well. Moreover,

2590-503: Is another classically valid , simple argument form . Intuitively, it permits the inference from any conjunction of either element of that conjunction. ...or alternatively, In logical operator notation: ...or alternatively, A conjunction A ∧ B {\displaystyle A\land B} is proven false by establishing either ¬ A {\displaystyle \neg A} or ¬ B {\displaystyle \neg B} . In terms of

2664-440: Is called structural . (Note that the term "structural" as used here and below is unrelated to the notion of structural rules in sequent calculi .) A structural consequence relation is called a propositional logic . A formula A is a theorem of a logic ⊢ {\displaystyle \vdash } if ∅ ⊢ A {\displaystyle \varnothing \vdash A} . For example, we identify

2738-404: Is called a substitution instance , or instance for short, of the original expression. Where ψ and φ represent formulas of propositional logic , ψ is a substitution instance of φ if and only if ψ may be obtained from φ by substituting formulas for propositional variables in φ , replacing each occurrence of the same variable by an occurrence of the same formula. For example:

2812-511: Is commonly represented by an infix operator, usually as a keyword such as " AND ", an algebraic multiplication, or the ampersand symbol & (sometimes doubled as in && ). Many languages also provide short-circuit control structures corresponding to logical conjunction. Logical conjunction is often used for bitwise operations, where 0 corresponds to false and 1 to true: The operation can also be applied to two binary words viewed as bitstrings of equal length, by taking

2886-483: Is equal to { y  ↦ 3+4, x  ↦ 2 }, but different from { x  ↦ 2, y  ↦ 7 }. The substitution { x  ↦  y + y } is idempotent, e.g. (( x + y ) { x ↦ y + y }) { x ↦ y + y } = (( y + y )+ y ) { x ↦ y + y } = ( y + y )+ y , while the substitution { x  ↦  x + y } is non-idempotent, e.g. (( x + y ) { x ↦ x + y }) { x ↦ x + y } = (( x + y )+ y ) { x ↦ x + y } = (( x + y )+ y )+ y . An example for non-commuting substitutions

2960-628: Is obtained by removing from the substitution { x 1  ↦  t 1 τ , …, x k  ↦  t k τ , y 1  ↦  u 1 , …, y l  ↦  u l } those pairs y i  ↦  u i for which y i ∈ { x 1 , …, x k }. The composition of σ and τ is denoted by στ . Composition is an associative operation , and is compatible with substitution application, i.e. ( ρσ ) τ = ρ ( στ ), and ( tσ ) τ = t ( στ ), respectively, for every substitutions ρ , σ , τ , and every term t . The identity substitution , which maps every variable to itself,

3034-440: Is often defined as having the result true. The truth table of A ∧ B {\displaystyle A\land B} : In systems where logical conjunction is not a primitive, it may be defined as It can be checked by the following truth table (compare the last two columns): or It can be checked by the following truth table (compare the last two columns): As a rule of inference, conjunction introduction

Admissible rule - Misplaced Pages Continue

3108-500: Is structurally complete, but it is included in the structurally incomplete logic KC . A rule with parameters is a rule of the form whose variables are divided into the "regular" variables p i , and the parameters s i . The rule is L -admissible if every L -unifier σ of A such that σs i  =  s i for each i is also a unifier of B . The basic decidability results for admissible rules also carry to rules with parameters. A multiple-conclusion rule

3182-555: Is the neutral element of substitution composition. A substitution σ is called idempotent if σσ = σ , and hence tσσ = tσ for every term t . When x i ≠ t i for all i , the substitution { x 1  ↦  t 1 , …, x k  ↦  t k } is idempotent if and only if none of the variables x i occurs in any t j . Substitution composition is not commutative, that is, στ may be different from τσ , even if σ and τ are idempotent. For example, { x  ↦ 2, y  ↦ 3+4 }

3256-400: Is the most modern and widely used. The and of a set of operands is true if and only if all of its operands are true, i.e., A ∧ B {\displaystyle A\land B} is true if and only if A {\displaystyle A} is true and B {\displaystyle B} is true. An operand of a conjunction is a conjunct . Beyond logic,

3330-395: Is typically represented as ∧ {\displaystyle \wedge } or & {\displaystyle \&} or K {\displaystyle K} (prefix) or × {\displaystyle \times } or ⋅ {\displaystyle \cdot } in which ∧ {\displaystyle \wedge }

3404-461: Is { x  ↦  y } { y  ↦  z } = { x  ↦  z , y  ↦  z }, but { y  ↦  z } { x  ↦  y } = { x  ↦  y , y  ↦  z }. In mathematics , there are two common uses of substitution: substitution of variables for constants (also called assignment for that variable), and the substitution property of equality , also called Leibniz's Law . Considering mathematics as

3478-488: The Gödel–McKinsey–Tarski translation : Rybakov (1997) developed much more sophisticated techniques for showing decidability of admissibility, which apply to a robust (infinite) class of transitive (i.e., extending K 4 or IPC ) modal and superintuitionistic logics, including e.g. S 4.1, S 4.2, S 4.3, KC , T k (as well as the above-mentioned logics IPC , K 4, S 4, GL , Grz ). Despite being decidable,

3552-429: The equational theory of modal or Heyting algebras . The connection was developed by Ghilardi (1999, 2000). In the logical setup, a unifier of a formula A in the language of a logic L (an L -unifier for short) is a substitution σ such that σA is a theorem of L . (Using this notion, we can rephrase admissibility of a rule A / B in L as "every L -unifier of A is an L -unifier of B ".) An L -unifier σ

3626-588: The reduced form of rules . A modal rule in variables p 0 , ... , p k is called reduced if it has the form where each ¬ i , j u {\displaystyle \neg _{i,j}^{u}} is either blank, or negation ¬ {\displaystyle \neg } . For each rule r , we can effectively construct a reduced rule s (called the reduced form of r ) such that any logic admits (or derives) r if and only if it admits (or derives) s , by introducing extension variables for all subformulas in A , and expressing

3700-496: The x i must be pairwise distinct. Most authors additionally require each term t i to be syntactically different from x i , to avoid infinitely many distinct notations for the same substitution. Applying that substitution to a term t is written in postfix notation as t { x 1  ↦  t 1 , ..., x k  ↦  t k }; it means to (simultaneously) replace every occurrence of each x i in t by t i . The result tσ of applying

3774-440: The accent in algebra is on the preservation of algebraic structure by the substitution operation, the fact that substitution gives a homomorphism for the structure at hand (in the case of polynomials, the ring structure). Substitution is a basic operation in algebra , in particular in computer algebra . A common case of substitution involves polynomials , where substitution of a numerical value (or another expression) for

SECTION 50

#1732772272081

3848-405: The admissibility problem has relatively high computational complexity , even in simple logics: admissibility of rules in the basic transitive logics IPC , K 4, S 4, GL , Grz is coNEXP -complete. This should be contrasted with the derivability problem (for rules or formulas) in these logics, which is PSPACE -complete. Admissibility in propositional logics is closely related to unification in

3922-421: The bitwise AND of each pair of bits at corresponding positions. For example: This can be used to select part of a bitstring using a bit mask . For example, 1001 1 101 AND 0000 1 000  =  0000 1 000 extracts the fourth bit of an 8-bit bitstring. In computer networking , bit masks are used to derive the network address of a subnet within an existing network from a given IP address , by ANDing

3996-445: The case of superintuitionistic logics , or { → , ⊥ , ◻ } {\displaystyle \{\to ,\bot ,\Box \}} in the case of monomodal logics ). Well-formed formulas are built freely using these connectives from a countably infinite set of propositional variables p 0 , p 1 , .... A substitution σ is a function from formulas to formulas that commutes with applications of

4070-673: The conjunction false: In other words, a conjunction can actually be proven false just by knowing about the relation of its conjuncts, and not necessary about their truth values. This formula can be seen as a special case of when C {\displaystyle C} is a false proposition. Either of the above are constructively valid proofs by contradiction. commutativity : yes associativity : yes distributivity : with various operations, especially with or with exclusive or : with material nonimplication : with itself: idempotency : yes monotonicity : yes truth-preserving: yes When all inputs are true,

4144-465: The connectives, i.e., for every connective f , and formulas A 1 , ... , A n . (We may also apply substitutions to sets Γ of formulas, making σ Γ = { σA : A ∈ Γ}. ) A Tarski-style consequence relation is a relation ⊢ {\displaystyle \vdash } between sets of formulas, and formulas, such that for all formulas A , B , and sets of formulas Γ, Δ. A consequence relation such that for all substitutions σ

4218-438: The existence of unique homomorphisms that send indeterminates to specific values; the substitution then amounts to finding the image of an element under such a homomorphism. Logical conjunction In logic , mathematics and linguistics , and ( ∧ {\displaystyle \wedge } ) is the truth-functional operator of conjunction or logical conjunction . The logical connective of this operator

4292-474: The following is true for every valuation ⊩ {\displaystyle \Vdash } in F : (The definition readily generalizes to general frames , if needed.) Let X be a subset of W , and t a point in W . We say that t is We say that a frame F has reflexive (irreflexive) tight predecessors, if for every finite subset X of W , there exists a reflexive (irreflexive) tight predecessor of X in W . We have: Note that apart from

4366-668: The indeterminate of a univariate polynomial amounts to evaluating the polynomial at that value. Indeed, this operation occurs so frequently that the notation for polynomials is often adapted to it; instead of designating a polynomial by a name like P , as one would do for other mathematical objects, one could define so that substitution for X can be designated by replacement inside " P ( X )", say or Substitution can also be applied to other kinds of formal objects built from symbols, for instance elements of free groups . In order for substitution to be defined, one needs an algebraic structure with an appropriate universal property , that asserts

4440-752: The latter term cannot be transformed back to x + y , as the information about the origin a z stems from is lost. The ground substitution { x  ↦ 2 } cannot have an inverse due to a similar loss of origin information e.g. in ( x +2) { x  ↦ 2 } = 2+2, even if replacing constants by variables was allowed by some fictitious kind of "generalized substitutions". Two substitutions are considered equal if they map each variable to syntactically equal result terms, formally: σ = τ if xσ = xτ for each variable x ∈ V . The composition of two substitutions σ = { x 1  ↦  t 1 , …, x k  ↦  t k } and τ = { y 1  ↦  u 1 , …, y l  ↦ u l }

4514-470: The latter term is usually reserved for philosophical contexts), generally states that, if two things are equal, then any property of one, must be a property of the other. It can be formally stated in logical notation as: ( a = b ) ⟹ [ ϕ ( a ) ⇒ ϕ ( b ) ] {\displaystyle (a=b)\implies {\bigl [}\phi (a)\Rightarrow \phi (b){\bigr ]}} For every

SECTION 60

#1732772272081

4588-461: The logic. A structural inference rule (or just rule for short) is given by a pair (Γ, B ), usually written as where Γ = { A 1 , ... , A n } is a finite set of formulas, and B is a formula. An instance of the rule is for a substitution σ . The rule Γ/ B is derivable in ⊢ {\displaystyle \vdash } , if Γ ⊢ B {\displaystyle \Gamma \vdash B} . It

4662-417: The object language, this reads This formula can be seen as a special case of when C {\displaystyle C} is a false proposition. If A {\displaystyle A} implies ¬ B {\displaystyle \neg B} , then both ¬ A {\displaystyle \neg A} as well as A {\displaystyle A} prove

4736-459: The one hand, the set of all admissible rules is a recursive basis if admissibility is decidable. On the other hand, the set of admissible rules is always co-recursively enumerable, and if we further have a recursively enumerable basis, set of admissible rules is also recursively enumerable; hence it is decidable. (In other words, we can decide admissibility of A / B by the following algorithm : we start in parallel two exhaustive searches , one for

4810-457: The operator is K {\displaystyle K} , for Polish koniunkcja . In mathematics, the conjunction of an arbitrary number of elements a 1 , … , a n {\displaystyle a_{1},\ldots ,a_{n}} can be denoted as an iterated binary operation using a "big wedge" ⋀ (Unicode U+22C0 ⋀ N-ARY LOGICAL AND ): ⋀ i = 1 n

4884-401: The output is true. falsehood-preserving: yes When all inputs are false, the output is false. Walsh spectrum : (1,-1,-1,1) Non linearity : 1 (the function is bent ) If using binary values for true (1) and false (0), then logical conjunction works exactly like normal arithmetic multiplication . In high-level computer programming and digital electronics , logical conjunction

4958-474: The previous section. In first-order logic , a substitution is a total mapping σ : V → T from variables to terms ; many, but not all authors additionally require σ ( x ) = x for all but finitely many variables x . The notation { x 1  ↦  t 1 , …, x k  ↦  t k } refers to a substitution mapping each variable x i to the corresponding term t i , for i =1,…, k , and every other variable to itself;

5032-453: The proof provides an explicit construction of an MGU for a given projective formula A . In the basic transitive logics IPC , K 4, S 4, GL , Grz (and more generally in any transitive logic with the finite model property whose set of finite frame satisfies another kind of extension property), we can effectively construct for any formula A its projective approximation Π( A ): a finite set of projective formulas such that It follows that

5106-477: The result in the full disjunctive normal form . It is thus sufficient to construct a decision algorithm for admissibility of reduced rules. Let ⋁ i = 0 n φ i / p 0 {\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}} be a reduced rule as above. We identify every conjunction φ i {\displaystyle \varphi _{i}} with

5180-522: The set { ¬ i , j 0 p j , ¬ i , j 1 ◻ p j ∣ j ≤ k } {\displaystyle \{\neg _{i,j}^{0}p_{j},\neg _{i,j}^{1}\Box p_{j}\mid j\leq k\}} of its conjuncts. For any subset W of the set { φ i ∣ i ≤ n } {\displaystyle \{\varphi _{i}\mid i\leq n\}} of all conjunctions, let us define

5254-476: The set of MGUs of elements of Π( A ) is a complete set of unifiers of A . Furthermore, if P is a projective formula, then for any formula B . Thus we obtain the following effective characterization of admissible rules: Let L be a logic. A set R of L -admissible rules is called a basis of admissible rules, if every admissible rule Γ/ B can be derived from R and the derivable rules of L , using substitution, composition, and weakening. In other words, R

5328-481: The set { x , y } as its domain. An example for a renaming substitution is { x  ↦  x 1 , x 1  ↦  y , y  ↦  y 2 , y 2  ↦  x }, it has the inverse { x  ↦  y 2 , y 2  ↦  y , y  ↦  x 1 , x 1  ↦  x }. The flat substitution { x  ↦  z , y  ↦  z } cannot have an inverse, since e.g. ( x + y ) { x  ↦  z , y  ↦  z } = z + z , and

5402-613: The term "conjunction" also refers to similar concepts in other fields: And is usually denoted by an infix operator: in mathematics and logic, it is denoted by a "wedge" ∧ {\displaystyle \wedge } (Unicode U+2227 ∧ LOGICAL AND ), & {\displaystyle \&} or × {\displaystyle \times } ; in electronics, ⋅ {\displaystyle \cdot } ; and in programming languages, & , && , or and . In Jan Łukasiewicz 's prefix notation for logic ,

5476-498: Was given respectively by Citkin and Rybakov. Namely, a superintuitionistic logic is hereditarily structurally complete if and only if it is not valid in any of the five Kripke frames Similarly, an extension of K 4 is hereditarily structurally complete if and only if it is not valid in any of certain twenty Kripke frames (including the five intuitionistic frames above). There exist structurally complete logics that are not hereditarily structurally complete: for example, Medvedev's logic

#80919