A solver for finding the maximum size of "nice" (complete and independent) sets of logical connectives in classical two-valued logic.
Status: Fully Implemented | Tests: 175 passing
- Installation - Platform-specific installation guide
- Usage Guide - Complete command reference and workflows
- Jupyter Notebooks - Interactive tutorials and examples
- Claude Code Guide - Using AI assistance with this codebase
- Results - Research findings (truth-functional: size-33, syntactic: size-35)
- Examples - Real execution examples and output
- Implementation - CLI and code documentation
- Testing - Test suite documentation
- Specs - Research reports and implementation plans
- Glossary - Complete ternary connectives reference
- Problem Statement
- Answer
- Quick Start
- Results Summary
- Technical Approach
- Project Structure
- Documentation
- Contributing
- References
Given classical two-valued connectives of arbitrary arity, we define a set of connectives as nice if it is:
- Complete: Every classical connective is definable from the set (via Post's Completeness Theorem)
- Independent: No connective in the set is definable from the other connectives
What is the largest size of a nice set?
Using Z3-based constraint solving with pattern enumeration (composition depth 3):
The maximum size depends on the definability mode used:
Truth-Functional Mode (Default - Clone-Theoretic):
- Binary-only (arity ≤2): Maximum size varies by mode
- Unary + Binary (arity ≤2): Maximum size is 5 (proven via Z3 exhaustive search)
- Up to Ternary (arity ≤3): Nice sets of size 33 verified (likely maximum)
- Higher arities (≥4): Unexplored - quaternary functions may enable different results
Syntactic Mode (Composition-Based):
- Binary-only (arity ≤2): Maximum size is 3 (classical result, proven and reproduced)
- Unary + Binary (arity ≤2): Maximum size is 5 (proven via Z3 exhaustive search)
- Up to Ternary (arity ≤3): Nice sets of size 35 verified (size-36+ unknown)
- Higher arities (≥4): Unexplored - quaternary functions may enable even larger nice sets
Why the difference? Truth-functional mode uses universal projection rules and cross-arity constant equivalence, detecting more dependencies and producing smaller maximum nice sets. See docs/DEFINABILITY.md for details.
See docs/RESULTS.md for complete research findings and verification details.
# Clone the repository
git clone <repository-url>
cd nice_connectives
# Install dependencies
pip install -e .
# On NixOS, use directly without installation
# (pip install doesn't work with read-only /nix/store)
# nix-shell -p python3 python3Packages.pytest python3Packages.z3
# python3 -m src.cli --helpSee docs/INSTALLATION.md for detailed installation instructions, including platform-specific guidance for Linux, macOS, Windows, and NixOS.
# Validate a known size-16 nice set
python -m src.cli search validate
# Search for nice sets with binary connectives only (finds max = 3)
python -m src.cli search binary
# Search with full arity support (finds size ≥ 16)
python -m src.cli search full --max-arity 3
# Run Z3-based proof
python -m src.cli prove z3
# Run enumeration-based proof
python -m src.cli prove enum
# Validate search results
python -m src.cli validate binary
python -m src.cli validate ternary
# Run benchmarks
python -m src.cli benchmark quick
python -m src.cli benchmark full
# Run test suite
pytest tests/ -v
# Get help on any command
python -m src.cli --help
python -m src.cli search --help
python -m src.cli prove z3 --helpSee docs/USAGE.md for complete usage guide and src/README.md for CLI and implementation documentation.
| Arity Range | Known Nice Sets | Example |
|---|---|---|
| Binary only (arity ≤2) | Mode-dependent | Varies by mode |
| Unary + Binary (arity ≤2) | Max size = 5 (proven) | {FALSE, TRUE, XOR, AND, IMP} |
| Up to Ternary (arity ≤3) | Size = 33 (likely max) | 1 constant + 1 binary + 31 ternary (94% ternary) |
| Higher arities (arity ≥4) | Unexplored | Quaternary+ may enable different results |
| Arity Range | Known Nice Sets | Example |
|---|---|---|
| Binary only (arity ≤2) | Max size = 3 (proven) | {XOR, AND, TRUE} |
| Unary + Binary (arity ≤2) | Max size = 5 (proven) | {FALSE, TRUE, XOR, AND, IMP} |
| Up to Ternary (arity ≤3) | Size ≥ 35 | 1 constant + 1 binary + 33 ternary (94% ternary) |
| Higher arities (arity ≥4) | Unexplored | Quaternary+ may enable larger sets |
- Definability mode matters - truth-functional (default) gives size-33, syntactic gives size-35
- Truth-functional is more restrictive - universal projections and cross-arity constants create more dependencies
- Ternary functions essential - in both modes, ternary functions dominate large nice sets (90%+)
- Pattern enumeration effective - depth 3 composition checking verifies independence
- Validated implementation - reproduces known results in both modes
- Mode choice matters for research - choose based on whether you want clone-theoretic or composition-based results
| Target Size | Max Arity | Result | Complete Sets Checked | Search Time | Notes |
|---|---|---|---|---|---|
| 3 (binary-only) | 2 | ✓ Found | ~560 | <1s | Classical result validated |
| 5 (unary+binary) | 2 | ✓ Found | ~2,300 | 0.04s | Z3 symmetry breaking effective |
| 17 | 3 | ✓ Found | 22 | 0.69s | First ternary inclusion |
| 29 | 3 | ✓ Found | 161 | 3.17s | Early ternary dominance |
| 30 | 3 | ✓ Found | 1,246 | 245.75s | 4 minutes |
| 31 | 3 | ✓ Found | 9,527 | 359.62s | 6 minutes - slowest in 31-34 range |
| 32 | 3 | ✓ Found | 1,822 | 35.93s | 10× faster than 31! Non-monotonic |
| 33 | 3 | ✓ Found | 1,239 | 24.15s | Fastest in series |
| 34 | 3 | ✓ Found | 3,226 | 86.69s | Moderate difficulty |
| 35 | 3 | ✓ Found | 26,860 | 2783.17s (~46 min) | 8× harder, sparse solutions |
| 36 | 3 | ? Unknown | - | - | May require extended search or may not exist |
| Target Size | Max Arity | Result | Search Time | Notes |
|---|---|---|---|---|
| 29 | 3 | ✓ Found | ~3s | Truth-functional mode |
| 32 | 3 | ✓ Found | ~36s | Truth-functional mode |
| 33 | 3 | ✓ Found | ~24s | Likely maximum for truth-functional |
Key Observations:
- Mode affects maximum size: Truth-functional detects more dependencies → smaller maximum (33 vs 35)
- Non-monotonic complexity: Larger sizes aren't always harder (size-32 much faster than size-31)
- Solution space collapsing: Higher sizes show exponentially more candidates needed
- Default is truth-functional: All commands use truth-functional mode unless
--definability-mode syntacticis specified
See docs/RESULTS.md for complete findings and examples/README.md for detailed examples.
1. BitVec Encoding
- Truth tables encoded as integers for compact storage and fast equality checks
- Example: AND (arity 2) = 0b1000 = 8
2. Post's Completeness Theorem
- Complete ↔ Escape all 5 maximal clones (T0, T1, M, D, A)
- O(n) completeness check vs exponential definability check
3. Bounded Composition via Pattern Enumeration
- Check definability up to depth d using explicit pattern matching
- Depth 3 balances thoroughness with performance
4. Incremental Arity Search
- Start with binary (16 functions) → max = 3 (proven)
- Add constants + unary (2 + 4 functions) → max = 5 (proven)
- Add ternary (256 functions) → size ≥ 30 (found via Z3)
See src/README.md for complete implementation details.
nice_connectives/
├── src/ # Source code
│ ├── cli.py # Unified CLI entry point
│ ├── commands/ # CLI command implementations
│ │ ├── prove.py # Proof commands (z3, enum)
│ │ ├── validate.py # Validation commands (binary, ternary)
│ │ ├── benchmark.py # Benchmark commands (full, quick, depth)
│ │ └── search.py # Search commands (binary, full, validate)
│ ├── proofs/ # Formal proof scripts
│ │ ├── z3_proof.py # Z3 constraint solver-based proof
│ │ ├── enumeration_proof.py # Pattern enumeration-based proof
│ │ └── README.md # Proof methodology documentation
│ ├── connectives.py # BitVec truth table representation
│ ├── constants.py # Predefined connectives
│ ├── post_classes.py # Completeness checking
│ ├── independence.py # Independence checking
│ ├── search.py # Search algorithms
│ ├── main.py # Library interface
│ └── README.md # Implementation documentation
├── tests/ # Test suite (175 passing)
│ └── README.md # Testing documentation
├── examples/ # Real execution examples
│ └── README.md # Examples documentation
├── docs/ # Documentation
│ ├── INSTALLATION.md # Complete installation guide
│ ├── USAGE.md # Usage guide and command reference
│ └── RESULTS.md # Research findings and conclusion
├── specs/ # Research reports and plans
│ ├── reports/ # Research findings
│ ├── plans/ # Implementation plans
│ ├── summaries/ # Execution summaries
│ └── README.md # Specs organization
├── pyproject.toml # Package configuration
└── README.md # This file
All functionality is accessible through the unified CLI:
python -m src.cli <subcommand>(ornice-connectivesif installed)- See src/README.md for complete CLI documentation
- See src/commands/README.md for command implementation details
- See src/proofs/README.md for proof script details
Post, E. L. (1941). "The Two-Valued Iterative Systems of Mathematical Logic." Annals of Mathematics Studies, No. 5
- Proves completeness theorem for 5 maximal clones (T0, T1, M, D, A)
- Foundation for efficient completeness checking
-
Installation Guide - Complete setup instructions for all platforms
- Terminal basics for beginners
- Python 3, pytest, and z3-solver installation
- Platform-specific instructions (Linux, macOS, Windows, NixOS)
- Troubleshooting common issues
- Verification steps
-
Usage Guide - Comprehensive command reference
- All CLI commands with examples
- Expected outputs and results
- Common workflows
- Performance tips
- Advanced usage patterns
-
Definability Modes - Syntactic vs truth-functional definability
- Mathematical definitions of both modes
- Universal projections and cross-arity constants
- Practical examples showing differences
- When to use each mode
- CLI integration and usage
-
Research Results - Key findings and conclusions
- Binary-only: max = 3 (classical result)
- Unary + Binary: max = 5 (proven)
- With Ternary: size ≥ 30 (current verified maximum)
- Systematic search results and analysis
-
Examples - Detailed example outputs
- Binary-only enumeration - Exhaustive search finding all 76 nice sets
- Unary+Binary enumeration - Finding all 5 size-5 nice sets
- Classical binary analysis - Detailed walkthrough
- Z3 discoveries - Size-30 maximum (current record)
- Enumeration vs Z3 comparison
-
Source Code Documentation - Complete implementation guide
- Module organization and architecture
- CLI interface and commands
- Core algorithms (BitVec encoding, Post classes, independence checking)
- Performance characteristics
- API reference
-
Command Implementations - CLI command modules
- prove.py - Z3 and enumeration proofs
- search.py - Enumeration search algorithms
- validate.py - Result validation
- benchmark.py - Performance testing
-
Proof Scripts - Formal proof methodology
- Z3 constraint solving approach
- Enumeration proof strategy
- Important code blocks with explanations
- Test Suite - 175 passing tests
- Unit tests for core functionality
- Integration tests for search algorithms
- Proof validation tests
- Coverage information
- Specs - Research process documentation
We welcome contributions! Whether you've found a bug, have an improvement idea, or want to add new features, we're here to help you contribute successfully.
Complete guides available:
- GitHub Setup Guide - Fork the repository, set up SSH keys, and configure your development environment
- Contributing Guide - Complete workflow from creating a feature branch to submitting a pull request
Summary:
- Code Style: Follow existing patterns in the codebase (see CLAUDE.md)
- Testing: Add tests for new features (see tests/README.md)
- Documentation: Update relevant docs in
docs/and docstrings - Commits: Use clear, descriptive commit messages (see the Commit Guidelines section)
- Dependencies: Minimize new dependencies and justify if needed
Found a bug? Please open an issue with:
- Clear description of the problem
- Steps to reproduce
- Expected vs actual behavior
- Your environment (OS, Python version)
- Relevant error messages or logs
Have a question? Open an issue with the "question" label.
Interested in contributing but not sure where to start? Consider:
- Performance optimizations - Improve search algorithms
- Higher arities - Explore quaternary (arity 4) connectives
- Visualization - Enhanced result visualization tools
- Documentation - Tutorials, examples, or clarifications
- Testing - Additional test coverage or edge cases
- Jupyter notebooks - New educational content
Open an issue with your question or proposed contribution idea for discussion before starting significant work.
Project Status: Implementation complete | 175 tests passing | Truth-functional: size-33 (likely max) | Syntactic: size-35 verified | Definability modes fully integrated