How big is BCI fragment of BCK logic

DOI10.1093/LOGCOM/EXS017MaRDI QIDQ5300586zbMATH OpenOpenAlexFDO

Authors Paweł M. Idziak, Marek Zaionc, Katarzyna Grygiel

Publication date 27 June 2013

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1112.0643

zbMATH Keywords

analytic combinatoricsasymptotic probability in logicBCI logicBCK logic

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Abstract: We investigate quantitative properties of BCI and BCK logics. The first part of the paper compares the number of formulas provable in BCI versus BCK logics. We consider formulas built on implication and a fixed set of $k$ variables. We investigate the proportion between the number of such formulas of a given length $n$ provable in BCI logic against the number of formulas of length $n$ provable in richer BCK logic. We examine an asymptotic behavior of this fraction when length $n$ of formulas tends to infinity. This limit gives a probability measure that randomly chosen BCK formula is also provable in BCI. We prove that this probability tends to zero as the number of variables tends to infinity. The second part of the paper is devoted to the number of lambda terms representing proofs of BCI and BCK logics. We build a proportion between number of such proofs of the same length $n$ and we investigate asymptotic behavior of this proportion when length of proofs tends to infinity. We demonstrate that with probability 0 a randomly chosen BCK proof is also a proof of a BCI formula.

Recommendations

• The number of proofs for a BCK-formula
• scientific article; zbMATH DE number 517044
• On the asymptotic number of BCK(2)-terms
• Asymptotics and random sampling for BCI and BCK lambda terms
• Enumeration of generalized BCI lambda-terms

Cited in

(6)

• Enumerating lambda terms by weighted length of their de Bruijn representation
• The number of proofs for a BCK-formula
• On the number of variables in special classes of random lambda-terms
• Distribution of variables in lambda-terms with restrictions on De Bruijn indices and De Bruijn levels
• Asymptotic distribution of parameters in trivalent maps and linear lambda terms
• Self-implications in BCI

Describes a project that uses

Uses Software

• OEIS

This page was built for publication: How big is BCI fragment of BCK logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5300586)