Frege proof system and TNC°

1998 ◽  
Vol 63 (2) ◽  
pp. 709-738
Author(s):  
Gaisi Takeuti
Keyword(s):  
Modus Ponens ◽  
Free Variable ◽  
Proof System ◽  
Order System ◽  
Equational Logic ◽  
Separation Problem ◽  
Conservative Extension ◽  
First Order ◽  
Polynomial Size ◽  
Extension Axiom

A Frege proof systemFis any standard system of prepositional calculus, e.g., a Hilbert style system based on finitely many axiom schemes and inference rules. An Extended Frege systemEFis obtained fromFas follows. AnEF-sequence is a sequence of formulas ψ1, …, ψκsuch that eachψiis either an axiom ofF, inferred from previous ψuand ψv(= ψu→ ψi) by modus ponens or of the formq↔ φ, whereqis an atom occurring neither in φ nor in any of ψ1,…,ψi−1. Suchq↔ φ, is called an extension axiom andqa new extension atom. AnEF-proof is anyEF-sequence whose last formula does not contain any extension atom. In [12], S. A. Cook and R. Reckhow proved that the pigeonhole principlePHPhas a simple polynomial sizeEF-proof and conjectured thatPHPdoes not admit polynomial sizeF-proof. In [5], S. R. Buss refuted this conjecture by furnishing polynomial sizeF-proof forPHP. Since then the important separation problem of polynomial sizeFand polynomial sizeEFhas not shown any progress.In [11], S. A. Cook introduced the systemPV, a free variable equational logic whose provable functional equalities are ‘polynomial time verifiable’ and showed that the metamathematics ofFandEFcan be developed inPVand the soundness ofEFproved inPV. In [3], S. R. Buss introduced the first order systemand showed thatis essentially a conservative extension ofPV. There he also introduced a second order system(BD).

The substitution method

1965 ◽  
Vol 30 (2) ◽  
pp. 175-192 ◽  
Author(s):  
W. W. Tait
Keyword(s):  
Free Variable ◽  
Order System ◽  
Conservative Extension ◽  
Substitution Method ◽  
Recursive Definition ◽  
First Order ◽  
Variable Elimination ◽  
Primitive Recursion ◽  
Definition Of ◽  
Primitive Recursive

This paper deals with Hilbert's substitution method for eliminating bound variables from first order proofs. With a first order system S framed in the ε-calculus [2] the problem is to associate a system S' without bound variables and an effective procedure for transforming derivations in S into derivations in S′. The transform of a formula A derived in S is to be an “ε-substitution instance” of A, i.e. it is obtained by replacing terms εxB(x) in A by terms of S′. In general the choice of these terms will depend on the particular derivation of A, and not on A alone. Cf. [4]. The present formulation sharpens Hilbert's original statement of the problem, i.e. that the transform of A should be finitistically verifiable, by making explicit the methods of verification used, namely those formalized in S′; on the other hand, it generalizes Hilbert's formulation since S′ need not be restricted to finitist systems.The bound variable elimination procedure can always be taken to be primitive recursive in (the Gödel number of) the derivation of A. Constructions which transcend primitive recursion can simply be built into S′.In this paper we show that if S′ is taken to be a second order system with constants for functionals, then the existence of suitable ε-substitution instances can be expressed by the solvability of certain functional equations in S′. We deal with two cases here. If S is number theory without induction, i.e. essentially predicate calculus with identity, then we can solve the equations in question by taking for S′ the free variable part S* of S with an added rule of definition of functionals by cases (recursive definition on finite ordinals), which is a conservative extension of S*.

An Adjustment of Reference Tracking PID Controllers for a First-order System with a Dead Time

2016 ◽  
Vol 136 (5) ◽  
pp. 676-682 ◽  
Author(s):  
Akihiro Ishimura ◽  
Masayoshi Nakamoto ◽  
Takuya Kinoshita ◽  
Toru Yamamoto
Keyword(s):  
Dead Time ◽  
Order System ◽  
Pid Controllers ◽  
Reference Tracking ◽  
First Order

Relativized realizability in intuitionistic arithmetic of all finite types

1978 ◽  
Vol 43 (1) ◽  
pp. 23-44 ◽  
Author(s):  
Nicolas D. Goodman
Keyword(s):  
Extension Theorem ◽  
General Notion ◽  
Conservative Extension ◽  
First Order ◽  
New Information ◽  
Reflection Theorem ◽  
Order Arithmetic ◽  
Special Case ◽  
Dependent Choice ◽  
Intuitionistic Arithmetic

In this paper we introduce a new notion of realizability for intuitionistic arithmetic in all finite types. The notion seems to us to capture some of the intuition underlying both the recursive realizability of Kjeene [5] and the semantics of Kripke [7]. After some preliminaries of a syntactic and recursion-theoretic character in §1, we motivate and define our notion of realizability in §2. In §3 we prove a soundness theorem, and in §4 we apply that theorem to obtain new information about provability in some extensions of intuitionistic arithmetic in all finite types. In §5 we consider a special case of our general notion and prove a kind of reflection theorem for it. Finally, in §6, we consider a formalized version of our realizability notion and use it to give a new proof of the conservative extension theorem discussed in Goodman and Myhill [4] and proved in our [3]. (Apparently, a form of this result is also proved in Mine [13]. We have not seen this paper, but are relying on [12].) As a corollary, we obtain the following somewhat strengthened result: Let Σ be any extension of first-order intuitionistic arithmetic (HA) formalized in the language of HA. Let Σω be the theory obtained from Σ by adding functionals of finite type with intuitionistic logic, intensional identity, and axioms of choice and dependent choice at all types. Then Σω is a conservative extension of Σ. An interesting example of this theorem is obtained by taking Σ to be classical first-order arithmetic.

On the Boundary Value Problem in A Dihedral Angle for Normally Hyperbolic Systems of First Order

1998 ◽  
Vol 5 (2) ◽  
pp. 121-138
Author(s):  
O. Jokhadze
Keyword(s):  
Partial Differential Equations ◽  
Boundary Value Problem ◽  
Principal Part ◽  
Hyperbolic Systems ◽  
Boundary Value ◽  
Three Dimensional ◽  
Order System ◽  
First Order ◽  
Dimensional Boundary ◽  
Class Of Functions

Abstract Some structural properties as well as a general three-dimensional boundary value problem for normally hyperbolic systems of partial differential equations of first order are studied. A condition is given which enables one to reduce the system under consideration to a first-order system with the spliced principal part. It is shown that the initial problem is correct in a certain class of functions if some conditions are fulfilled.

scholarly journals Constructing weak simulations from linear implications for processes with private names

2019 ◽  
Vol 29 (8) ◽  
pp. 1275-1308 ◽  
Author(s):  
Ross Horne ◽  
Alwen Tiu
Keyword(s):  
Expressive Power ◽  
Dual Pair ◽  
Proof System ◽  
Branching Time ◽  
First Order ◽  
Order Extension

AbstractThis paper clarifies that linear implication defines a branching-time preorder, preserved in all contexts, when used to compare embeddings of process in non-commutative logic. The logic considered is a first-order extension of the proof system BV featuring a de Morgan dual pair of nominal quantifiers, called BV1. An embedding of π-calculus processes as formulae in BV1 is defined, and the soundness of linear implication in BV1 with respect to a notion of weak simulation in the π -calculus is established. A novel contribution of this work is that we generalise the notion of a ‘left proof’ to a class of formulae sufficiently large to compare embeddings of processes, from which simulating execution steps are extracted. We illustrate the expressive power of BV1 by demonstrating that results extend to the internal π -calculus, where privacy of inputs is guaranteed. We also remark that linear implication is strictly finer than any interleaving preorder.

Diffusion Experiments with a Global Discontinuous Galerkin Shallow-Water Model

2009 ◽  
Vol 137 (10) ◽  
pp. 3339-3350 ◽  
Author(s):  
Ramachandran D. Nair
Keyword(s):  
Shallow Water ◽  
Discontinuous Galerkin ◽  
Water Model ◽  
Order System ◽  
Small Scale ◽  
Shallow Water Model ◽  
First Order ◽  
Advection Diffusion Equation ◽  
Diffusion Scheme ◽  
Cubed Sphere

Abstract A second-order diffusion scheme is developed for the discontinuous Galerkin (DG) global shallow-water model. The shallow-water equations are discretized on the cubed sphere tiled with quadrilateral elements relying on a nonorthogonal curvilinear coordinate system. In the viscous shallow-water model the diffusion terms (viscous fluxes) are approximated with two different approaches: 1) the element-wise localized discretization without considering the interelement contributions and 2) the discretization based on the local discontinuous Galerkin (LDG) method. In the LDG formulation the advection–diffusion equation is solved as a first-order system. All of the curvature terms resulting from the cubed-sphere geometry are incorporated into the first-order system. The effectiveness of each diffusion scheme is studied using the standard shallow-water test cases. The approach of element-wise localized discretization of the diffusion term is easy to implement but found to be less effective, and with relatively high diffusion coefficients, it can adversely affect the solution. The shallow-water tests show that the LDG scheme converges monotonically and that the rate of convergence is dependent on the coefficient of diffusion. Also the LDG scheme successfully eliminates small-scale noise, and the simulated results are smooth and comparable to the reference solution.

Sign in / Sign up

Export Citation Format

Share Document