eprintid: 10199855
rev_number: 10
eprint_status: archive
userid: 699
dir: disk0/10/19/98/55
datestamp: 2024-11-11 12:25:49
lastmod: 2024-11-11 12:30:04
status_changed: 2024-11-11 12:25:49
type: article
metadata_visibility: show
sword_depositor: 699
creators_name: Kürbis, Nils
title: Normalisation for negative free logics without and with definite descriptions
ispublished: inpress
divisions: UCL
divisions: B03
divisions: C01
divisions: F16
keywords: Negative free logic; definite descriptions; 
proof theory; 
normalisation
note: Copyright © The Author(s), 2024. Published by Cambridge University Press on behalf of The Association for Symbolic Logic.
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
abstract: This paper proves normalisation theorems for intuitionist and classical negative free logic, without and with the  operator for definite descriptions. Rules specific to free logic give rise to new kinds of maximal formulas additional to those familiar from standard intuitionist and classical logic. When  is added it must be ensured that reduction procedures involving replacements of parameters by terms do not introduce new maximal formulas of higher degree than the ones removed. The problem is solved by a rule that permits restricting these terms in the rules for  ∀
 ,  ∃
  and  to parameters or constants. A restricted subformula property for deductions in systems without  is considered. It is improved upon by an alternative formalisation of free logic building on an idea of Jaśkowski’s. In the classical system the rules for  require treatment known from normalisation for classical logic with  ∨
  or  ∃
 . The philosophical significance of the results is also indicated.
date: 2024-09-03
date_type: published
publisher: CAMBRIDGE UNIV PRESS
official_url: http://dx.doi.org/10.1017/s1755020324000157
oa_status: green
full_text_type: pub
language: eng
primo: open
primo_central: open_green
verified: verified_manual
elements_id: 2312256
doi: 10.1017/S1755020324000157
lyricists_name: Kurbis, Nils
lyricists_id: NKURB54
actors_name: Kurbis, Nils
actors_id: NKURB54
actors_role: owner
funding_acknowledgements: 101054714 [European Union (ERC, ExtenDD)]
full_text_status: public
publication: The Review of Symbolic Logic
pagerange: 1-33
pages: 33
issn: 1755-0203
citation:        Kürbis, Nils;      (2024)    Normalisation for negative free logics without and with definite descriptions.                   The Review of Symbolic Logic     pp. 1-33.    10.1017/S1755020324000157 <https://doi.org/10.1017/S1755020324000157>.    (In press).    Green open access   
 
document_url: https://discovery.ucl.ac.uk/id/eprint/10199855/1/Kurbis_normalisation-for-negative-free-logics-without-and-with-definite-descriptions.pdf