Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems

Autor:	Ronald Harrop
Rok vydání:	1960
Předmět:	Algebra Set (abstract data type) Numeral system Discrete mathematics Philosophy Number theory Logic If and only if Type (model theory) Modus ponens Formal system Mathematics
Zdroj:	Journal of Symbolic Logic. 25:27-32
ISSN:	1943-5886 0022-4812
DOI:	10.2307/2964334
Popis:	In a previous paper [1] it was proved, among other results, that a closed disjunction of intuitionistic elementary number theory N can be proved if and only if at least one of its disjunctands is provable and that a closed formula of the type (Ex)B(x) is provable in N if and only if B(n) is provable for some numeral n. The method of proof was to show that, as far as closed formulas are concerned, N is equivalent to a calculus N1 for which the result is immediate. The main step in the proof consisted in showing that the set of provable formulas of N1 is closed under modus ponens. This was done by obtaining a subset of the set which is closed under modus ponens and contains all members of the original set, with which it is therefore identical.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::c3bdb54764c7111ade3526795c59749d https://doi.org/10.2307/2964334 Zobrazit plný text záznamu