Sistem Formal sebagai Graf Terarah
Suatu sistem axiom formal mengdefinisikan graf terarah:
- Titik: semua rumus yang baik dan rapi yang dapat dibangun dari simbol sistem
- Tebing: langkah inferensi — satu rumus mengikuti lain berdasarkan aturan inferensi
- Aksiom: titik sumber yang ditandai tanpa adanya tebing masuk
- Teorema: semua titik yang dapat dicapai dari set aksiom
Suatu bukti dari teorema T: sebuah jalur terarah dari set aksiom ke T. Bukti adalah sebuah urutan titik A₁, A₂, ..., Aₙ = T di mana setiap langkah mengikuti aturan inferensi.
Dua sifat fundamental dari suatu sistem formal, dinyatakan secara geometris:
Konsistensi: tidak ada rumus F dan negasinya ¬F yang keduanya dapat dicapai dari aksiom. Geometris: titik teorema F dan titik teorema ¬F tidak dapat dicapai. Tidak ada 'ledakan' jalur yang ada.
Keseluruhan: setiap rumus F atau ¬F adalah teorema (dapat dicapai). Geometris: graf tersebut kuat terhubung dalam arti bahwa untuk setiap titik F, setidaknya salah satu F atau ¬F memiliki jalur dari aksiom.
Kekacauan Gödel sebagai Sifat Geometris
Kurt Gödel membuktikan pada tahun 1931 bahwa sistem formal yang cukup kuat untuk mengungkapkan aritmatika dasar adalah tidak lengkap: ada rumus G sehingga tidak ada yang dapat dibuktikan G atau ¬G.
Geometris: dalam sistem formal yang cukup kaya dan konsisten, ada titik dalam graf rumus yang tidak dapat dicapai dari aksiom — titik G atau titik ¬G tidak memiliki jalur dari set aksiom.
Konstruksi Gödel: dia mengkodekan rumus G yang mengatakan, secara efektif, 'Saya tidak dapat dibuktikan.' Jika G dapat dibuktikan, sistem akan tidak konsisten (pernyataan yang benar mengatakan bahwa tidak dapat dibuktikan). Jika ¬G dapat dibuktikan, sistem akan tidak konsisten (G akan salah tetapi sistem membuktikannya). Jadi, tidak ada yang dapat dibuktikan G atau ¬G — G adalah titik yang tidak dapat dicapai dalam sistem yang konsisten.
Keterlaksanaan tidak merupakan kecacatan dari postulat yang dipilih: Gödel menunjukkan bahwa ini adalah sifat struktural dari sistem konsisten apa pun yang cukup ekspresif untuk menangani aritmetika. Verteks-verteks yang tidak dapat dijangkau tidak dapat dihapus dengan menambahkan lebih banyak postulat tanpa menghasilkan yang baru.
Objek Matematis sebagai Titik dalam Ruang
Pandangan Platonis tentang matematika dapat diformalkan secara geometris: objek matematis menghuni ruang abstrak di mana titik-titik adalah objek itu sendiri dan struktur diberikan oleh hubungan di antaranya.
Sertakan bilangan alami ℕ = {0, 1, 2, 3, ...}. Hubungan pembagian menentukan urutan sebagian: m membagi n jika m | n. Urutan ini menentukan geometri — diagram Hasse dari lattice kebolehan.
Setiap bilangan prima berada pada posisi minimal di atas 1. Setiap bilangan komposit berada di atas faktor prima-nya. Struktur ruang ini mengkode semua teori bilangan.
Apa yang membuat ini Platonis: struktur ini ada meskipun tidak ada pikiran yang mempelajarinya. Fakta bahwa 7 adalah prima — bahwa 7 tidak memiliki pembagi antara 1 dan 7 — adalah fakta tentang posisi 7 dalam lattice kebolehan, independen dari notasi, budaya, atau peradaban.
Setiap peradaban yang mengkaji bilangan dan ketidaksamaan akan menemukan struktur yang sama. Geometri sistem bilangan adalah universal.
Menavigasi Jaringan Ketidaksamaan
Dalam jaringan ketidaksamaan, bilangan terkecil umum (lcm) dari dua bilangan mewakili join (batas atas terendah) dan bilangan terbesar umum pembagi (gcd) mewakili meet (batas bawah terbesar).
gcd dapat dihitung menggunakan algoritma Euklides: gcd(a, b) = gcd(b, a mod b), hingga b = 0.
Apa yang Disingkirkan Abstraksi
Abstraksi geometri: memproyeksikan objek multidimensional ke subspasial berdimensi lebih rendah. Proyeksi kehilangan informasi (koordinat yang tidak ada di subspasial) tetapi mempertahankan struktur subspasial sempurna.
Abstraksi matematis bekerja dengan cara yang sama. Grup adalah himpunan dengan satu operasi biner yang memenuhi empat axiom. Mengabstraksikan ke struktur grup menghilangkan: elemen khusus, aturan komputasi operasi khusus, struktur tambahan (urutan, metrik, topologi). Yang tersisa: kerangka empat-axiom.
Hasilnya: setiap teorema tentang grup berlaku untuk SEMUA grup - bilangan bulat di bawah penambahan, rotasi di bawah komposisi, permutasi di bawah komposisi, simetri molekul, grup Galois persamaan polynomial - secara bersamaan. Teorema abstrak dapat dibuktikan sekali; instansnya gratis.
Itulah mengapa matematikawan murni menolak menambahkan asumsi domain: setiap asumsi yang ditambahkan mengurangi ketersediaan teorema. Sebuah teorema tentang lapangan (menambah invers multipikatif) berlaku pada struktur yang lebih sedikit dibandingkan sebuah teorema tentang ring (tidak diperlukan invers multipikatif).
Tradesoff Antara Presisi dan Jangkauan
Ada tradesoff: teorema-teorema yang lebih abstrak berlaku lebih luas tetapi mengatakan lebih sedikit tentang kasus-kasus khusus. Sebuah teorema tentang ruang vektor atas lapangan mengatakan lebih sedikit tentang ℝ^n dibandingkan sebuah teorema yang khusus untuk ℝ^n (di mana jarak dan sudut didefinisikan).
Aturan implisit Hamming: abstraklah sejauh mungkin sambil menahan properti yang Anda butuhkan. Abstrak terlalu jauh dan teorema-teorema Anda menjadi kosong umum ('setiap set dengan operasi apa pun memenuhi...'). Abstrak terlalu sedikit dan teorema-teorema Anda gagal ditransfer ke aplikasi baru.